<!DOCTYPE html>
<html class="writer-html5" lang="en" >
<head>
  <meta charset="utf-8" /><meta name="generator" content="Docutils 0.17.1: http://docutils.sourceforge.net/" />

  <meta name="viewport" content="width=device-width, initial-scale=1.0" />
  <title>9. Sets &mdash; The Mechanics of Proof, by Heather Macbeth</title>
      <link rel="stylesheet" href="_static/pygments.css" type="text/css" />
      <link rel="stylesheet" href="_static/css/theme.css" type="text/css" />
      <link rel="stylesheet" href="_static/css/custom.css" type="text/css" />
    <link rel="shortcut icon" href="_static/favicon.ico"/>
  <!--[if lt IE 9]>
    <script src="_static/js/html5shiv.min.js"></script>
  <![endif]-->
  
        <script data-url_root="./" id="documentation_options" src="_static/documentation_options.js"></script>
        <script src="_static/jquery.js"></script>
        <script src="_static/underscore.js"></script>
        <script src="_static/doctools.js"></script>
        <script async="async" src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script>
    <script src="_static/js/theme.js"></script>
    <link rel="index" title="Index" href="genindex.html" />
    <link rel="search" title="Search" href="search.html" />
    <link rel="next" title="10. Relations" href="10_Relations.html" />
    <link rel="prev" title="8. Functions" href="08_Functions.html" /> 
</head>

<body class="wy-body-for-nav"> 
  <div class="wy-grid-for-nav">
    <nav data-toggle="wy-nav-shift" class="wy-nav-side">
      <div class="wy-side-scroll">
        <div class="wy-side-nav-search" >
            <a href="index.html" class="icon icon-home"> The Mechanics of Proof
          </a>
<div role="search">
  <form id="rtd-search-form" class="wy-form" action="search.html" method="get">
    <input type="text" name="q" placeholder="Search docs" />
    <input type="hidden" name="check_keywords" value="yes" />
    <input type="hidden" name="area" value="default" />
  </form>
</div>
        </div><div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="Navigation menu">
              <ul>
<li class="toctree-l1"><a class="reference internal" href="00_Introduction.html">Preface</a></li>
</ul>
<ul class="current">
<li class="toctree-l1"><a class="reference internal" href="01_Proofs_by_Calculation.html">1. Proofs by calculation</a></li>
<li class="toctree-l1"><a class="reference internal" href="02_Proofs_with_Structure.html">2. Proofs with structure</a></li>
<li class="toctree-l1"><a class="reference internal" href="03_Parity_and_Divisibility.html">3. Parity and divisibility</a></li>
<li class="toctree-l1"><a class="reference internal" href="04_Proofs_with_Structure_II.html">4. Proofs with structure, II</a></li>
<li class="toctree-l1"><a class="reference internal" href="05_Logic.html">5. Logic</a></li>
<li class="toctree-l1"><a class="reference internal" href="06_Induction.html">6. Induction</a></li>
<li class="toctree-l1"><a class="reference internal" href="07_Number_Theory.html">7. Number theory</a></li>
<li class="toctree-l1"><a class="reference internal" href="08_Functions.html">8. Functions</a></li>
<li class="toctree-l1 current"><a class="current reference internal" href="#">9. Sets</a><ul>
<li class="toctree-l2"><a class="reference internal" href="#introduction">9.1. Introduction</a><ul>
<li class="toctree-l3"><a class="reference internal" href="#example">9.1.1. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id2">9.1.2. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id3">9.1.3. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id4">9.1.4. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id5">9.1.5. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id6">9.1.6. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id7">9.1.7. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id8">9.1.8. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id9">9.1.9. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#exercises">9.1.10. Exercises</a></li>
</ul>
</li>
<li class="toctree-l2"><a class="reference internal" href="#set-operations">9.2. Set operations</a><ul>
<li class="toctree-l3"><a class="reference internal" href="#union">9.2.1. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id12">9.2.2. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id13">9.2.3. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id14">9.2.4. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id15">9.2.5. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id16">9.2.6. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id17">9.2.7. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id18">9.2.8. Exercises</a></li>
</ul>
</li>
<li class="toctree-l2"><a class="reference internal" href="#the-type-of-sets">9.3. The type of sets</a><ul>
<li class="toctree-l3"><a class="reference internal" href="#definition">9.3.1. Definition</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id20">9.3.2. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id21">9.3.3. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id22">9.3.4. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id23">9.3.5. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id24">9.3.6. Exercises</a></li>
</ul>
</li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="10_Relations.html">10. Relations</a></li>
</ul>
<ul>
<li class="toctree-l1"><a class="reference internal" href="Index_of_Tactics.html">Index of Lean tactics</a></li>
<li class="toctree-l1"><a class="reference internal" href="Mainstream_Lean.html">Transitioning to mainstream Lean</a></li>
</ul>

        </div>
      </div>
    </nav>

    <section data-toggle="wy-nav-shift" class="wy-nav-content-wrap"><nav class="wy-nav-top" aria-label="Mobile navigation menu" >
          <i data-toggle="wy-nav-top" class="fa fa-bars"></i>
          <a href="index.html">The Mechanics of Proof</a>
      </nav>

      <div class="wy-nav-content">
        <div class="rst-content">
          <div role="navigation" aria-label="Page navigation">
  <ul class="wy-breadcrumbs">
      <li><a href="index.html" class="icon icon-home"></a> &raquo;</li>
      <li><span class="section-number">9. </span>Sets</li>
      <li class="wy-breadcrumbs-aside">
            <a href="_sources/09_Sets.rst.txt" rel="nofollow"> View page source</a>
      </li>
  </ul>
  <hr/>
</div>
          <div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article">
           <div itemprop="articleBody">
             
  <section id="sets">
<span id="id1"></span><h1><span class="section-number">9. </span>Sets<a class="headerlink" href="#sets" title="Permalink to this headline">&#61633;</a></h1>
<p>This chapter introduces the language of <em>sets</em>, a convenient way to reason about the
objects in a type which have some property.  This language includes
the concept of <em>membership</em> in a set, the property of a set being a <em>subset</em> of
another set, and a whole zoo of set operations, such as <em>intersection</em>, <em>union</em> and
<em>complement</em>, each of which is a wrapper for a logical symbol relating
the underlying properties.</p>
<p>In the last section of the chapter, <a class="reference internal" href="#powerset"><span class="std std-numref">Section 9.3</span></a>, we study the
collection of sets in a type as a type in its own right.</p>
<section id="introduction">
<span id="sets-intro"></span><h2><span class="section-number">9.1. </span>Introduction<a class="headerlink" href="#introduction" title="Permalink to this headline">&#61633;</a></h2>
<section id="example">
<h3><span class="section-number">9.1.1. </span>Example<a class="headerlink" href="#example" title="Permalink to this headline">&#61633;</a></h3>
<p>In type theory, the logical foundation for this book, a <em>set</em> in a type <span class="math notranslate nohighlight">\(X\)</span> is specified
by a predicate on <span class="math notranslate nohighlight">\(X\)</span>.  For example, &#8220;the set of integers <span class="math notranslate nohighlight">\(n\)</span> such that <span class="math notranslate nohighlight">\(n\le 3\)</span>&#8221;
is a set in <span class="math notranslate nohighlight">\(\mathbb{Z}\)</span>.</p>
<p>There is a standard notation for sets specified by predicates.  For example, the set described above
is written notationally as <span class="math notranslate nohighlight">\(\{n:\mathbb{Z} \mid n\le 3\}\)</span>. Here is that set in Lean.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span> <span class="o">{</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="n">n</span> <span class="bp">&#8804;</span> <span class="mi">3</span><span class="o">}</span>
</pre></div>
</div>
<p>Note that the infoview confirms that the type of the expression is <code class="docutils literal notranslate"><span class="pre">Set</span> <span class="pre">&#8484;</span></code>, a set of integers.</p>
<p>A term of type <span class="math notranslate nohighlight">\(X\)</span> <em>belongs to</em> a set in <span class="math notranslate nohighlight">\(X\)</span> specified by some predicate, if the
predicate holds for that term.</p>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Show that the integer 1 belongs to the set of integers <span class="math notranslate nohighlight">\(\{n:\mathbb{Z} \mid n\le 3\}\)</span>.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p><span class="math notranslate nohighlight">\(1\le 3\)</span>.</p>
</div>
<p>Other phrasings you may see for this concept are that 1 <em>is a member of</em> the set
<span class="math notranslate nohighlight">\(\{n:\mathbb{Z} \mid n\le 3\}\)</span>, or <em>is in</em> <span class="math notranslate nohighlight">\(\{n:\mathbb{Z} \mid n\le 3\}\)</span>.  The notation is
<span class="math notranslate nohighlight">\(1\in \{n:\mathbb{Z} \mid n\le 3\}\)</span>.</p>
<p>Here is this proof in Lean:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="mi">1</span> <span class="bp">&#8712;</span> <span class="o">{</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="n">n</span> <span class="bp">&#8804;</span> <span class="mi">3</span><span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span>
  <span class="n">numbers</span>
</pre></div>
</div>
<p>The tactic <code class="docutils literal notranslate"><span class="pre">dsimp</span></code> unfolds the definition of the set and of membership in that set, reducing it
to the goal</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="bp">&#8866;</span> <span class="mi">1</span> <span class="bp">&#8804;</span> <span class="mi">3</span>
</pre></div>
</div>
<p>which is resolved by <code class="docutils literal notranslate"><span class="pre">numbers</span></code>.</p>
</section>
<section id="id2">
<h3><span class="section-number">9.1.2. </span>Example<a class="headerlink" href="#id2" title="Permalink to this headline">&#61633;</a></h3>
<p>The symbol <span class="math notranslate nohighlight">\(\notin\)</span> is used for the negation of <span class="math notranslate nohighlight">\(\in\)</span>.</p>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Prove that <span class="math notranslate nohighlight">\(10\notin \{n:\mathbb{N} \mid n\text{ is odd}\}\)</span>.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>Since <span class="math notranslate nohighlight">\(10=2\cdot 5\)</span>, we have that 10 is even, so it is not odd.</p>
</div>
<p>In the Lean proof below, the tactic <code class="docutils literal notranslate"><span class="pre">dsimp</span></code> cleans up the goal to</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="bp">&#8866;</span> <span class="bp">&#172;</span><span class="n">Odd</span> <span class="mi">10</span>
</pre></div>
</div>
<p>which can then be solved by general-purpose methods.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="mi">10</span> <span class="bp">&#8713;</span> <span class="o">{</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">|</span> <span class="n">Odd</span> <span class="n">n</span><span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span>
  <span class="n">rw</span> <span class="o">[</span><span class="bp">&#8592;</span> <span class="n">even_iff_not_odd</span><span class="o">]</span>
  <span class="n">use</span> <span class="mi">5</span>
  <span class="n">numbers</span>
</pre></div>
</div>
</section>
<section id="id3">
<h3><span class="section-number">9.1.3. </span>Example<a class="headerlink" href="#id3" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-definition admonition">
<p class="admonition-title">Definition</p>
<p>Let <span class="math notranslate nohighlight">\(U\)</span> and <span class="math notranslate nohighlight">\(V\)</span> be sets in the type <span class="math notranslate nohighlight">\(X\)</span>.  The set <span class="math notranslate nohighlight">\(U\)</span> <em>is a subset of</em>
the set <span class="math notranslate nohighlight">\(V\)</span>, if for all <span class="math notranslate nohighlight">\(x\)</span> of type <span class="math notranslate nohighlight">\(X\)</span>, if <span class="math notranslate nohighlight">\(x\in U\)</span>, then <span class="math notranslate nohighlight">\(x\in V\)</span>.</p>
</div>
<p>The statement &#8220;<span class="math notranslate nohighlight">\(U\)</span> <em>is a subset of</em> <span class="math notranslate nohighlight">\(V\)</span>&#8221; is expressed in notation as
<span class="math notranslate nohighlight">\(U \subseteq V\)</span>.</p>
<p>In Lean the definition looks like this:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span> <span class="n">Set.Subset</span> <span class="o">(</span><span class="n">U</span> <span class="n">V</span> <span class="o">:</span> <span class="n">Set</span> <span class="n">&#945;</span><span class="o">)</span> <span class="o">:</span> <span class="kt">Prop</span> <span class="o">:=</span> <span class="bp">&#8704;</span> <span class="o">&#10627;</span><span class="n">x</span><span class="o">&#10628;,</span> <span class="n">x</span> <span class="bp">&#8712;</span> <span class="n">U</span> <span class="bp">&#8594;</span> <span class="n">x</span> <span class="bp">&#8712;</span> <span class="n">V</span>
</pre></div>
</div>
<p>and the notation is <code class="docutils literal notranslate"><span class="pre">U</span> <span class="pre">&#8838;</span> <span class="pre">V</span></code>.</p>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Show that <span class="math notranslate nohighlight">\(\{a:\mathbb{N} \mid 4\mid a\}\subseteq\{b:\mathbb{N} \mid 2\mid b\}\)</span>.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>We will show that for all natural numbers <span class="math notranslate nohighlight">\(a\)</span>, if <span class="math notranslate nohighlight">\(4\mid a\)</span> then <span class="math notranslate nohighlight">\(2\mid a\)</span>.
Indeed, let <span class="math notranslate nohighlight">\(a\)</span> be a natural number and suppose that <span class="math notranslate nohighlight">\(4\mid a\)</span>.  Then there exists a
natural number <span class="math notranslate nohighlight">\(k\)</span> such that <span class="math notranslate nohighlight">\(a=4k\)</span>, so</p>
<div class="math notranslate nohighlight">
\[\begin{split}a&amp;=4a\\
&amp;=2(2k),\end{split}\]</div>
<p>so <span class="math notranslate nohighlight">\(2\mid a\)</span>.</p>
</div>
<p>Here is that solution in Lean.  Note that after unfolding the definition using <code class="docutils literal notranslate"><span class="pre">dsimp</span></code>
the goal state is simplified to</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="bp">&#8866;</span> <span class="bp">&#8704;</span> <span class="o">(</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8469;</span><span class="o">),</span> <span class="mi">4</span> <span class="bp">&#8739;</span> <span class="n">x</span> <span class="bp">&#8594;</span> <span class="mi">2</span> <span class="bp">&#8739;</span> <span class="n">x</span>
</pre></div>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="o">{</span><span class="n">a</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">|</span> <span class="mi">4</span> <span class="bp">&#8739;</span> <span class="n">a</span><span class="o">}</span> <span class="bp">&#8838;</span> <span class="o">{</span><span class="n">b</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">|</span> <span class="mi">2</span> <span class="bp">&#8739;</span> <span class="n">b</span><span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Set.subset_def</span><span class="o">]</span> <span class="c1">-- optional</span>
  <span class="n">intro</span> <span class="n">a</span> <span class="n">ha</span>
  <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">k</span><span class="o">,</span> <span class="n">hk</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">ha</span>
  <span class="n">use</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">k</span>
  <span class="k">calc</span> <span class="n">a</span> <span class="bp">=</span> <span class="mi">4</span> <span class="bp">*</span> <span class="n">k</span> <span class="o">:=</span> <span class="n">hk</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="mi">2</span> <span class="bp">*</span> <span class="o">(</span><span class="mi">2</span> <span class="bp">*</span> <span class="n">k</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
</pre></div>
</div>
<p>You can also check that the proof goes through without the <code class="docutils literal notranslate"><span class="pre">dsimp</span></code> line.</p>
</section>
<section id="id4">
<h3><span class="section-number">9.1.4. </span>Example<a class="headerlink" href="#id4" title="Permalink to this headline">&#61633;</a></h3>
<p>The notation <span class="math notranslate nohighlight">\(\not\subseteq\)</span> stands for &#8220;not a subset of&#8221;.</p>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Prove that <span class="math notranslate nohighlight">\(\{x:\mathbb{R} \mid 0 \le x^2\}\not\subseteq \{t:\mathbb{R} \mid 0\le t\}\)</span>.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>We will show that there exists a real number <span class="math notranslate nohighlight">\(x\)</span>, such that <span class="math notranslate nohighlight">\(0\le x^2\)</span> and
<span class="math notranslate nohighlight">\(x&lt;0\)</span>.  Indeed, <span class="math notranslate nohighlight">\(0\le (-3)^2\)</span> and <span class="math notranslate nohighlight">\(-3&lt;0\)</span>.</p>
</div>
<p>In Lean, after unfolding the definitions and negation-normalizing, the goal shows as</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="bp">&#8866;</span> <span class="bp">&#8707;</span> <span class="n">x</span><span class="o">,</span> <span class="mi">0</span> <span class="bp">&#8804;</span> <span class="n">x</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">&#8743;</span> <span class="n">x</span> <span class="bp">&lt;</span> <span class="mi">0</span>
</pre></div>
</div>
<p>This is the reformulation we state in the first sentence of the text proof.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="o">{</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8477;</span> <span class="bp">|</span> <span class="mi">0</span> <span class="bp">&#8804;</span> <span class="n">x</span> <span class="bp">^</span> <span class="mi">2</span><span class="o">}</span> <span class="bp">&#8840;</span> <span class="o">{</span><span class="n">t</span> <span class="o">:</span> <span class="n">&#8477;</span> <span class="bp">|</span> <span class="mi">0</span> <span class="bp">&#8804;</span> <span class="n">t</span><span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Set.subset_def</span><span class="o">]</span>
  <span class="n">push_neg</span>
  <span class="n">use</span> <span class="bp">-</span><span class="mi">3</span>
  <span class="n">constructor</span>
  <span class="bp">&#183;</span> <span class="n">numbers</span>
  <span class="bp">&#183;</span> <span class="n">numbers</span>
</pre></div>
</div>
</section>
<section id="id5">
<h3><span class="section-number">9.1.5. </span>Example<a class="headerlink" href="#id5" title="Permalink to this headline">&#61633;</a></h3>
<p>To show that two sets are equal in Lean, we show that something is a member of one if and only if
it is a member of the other.  This is called the <em>set extensionality</em> property &#8211; compare with the
<em>functional extensionality</em> property discussed in <a class="reference internal" href="08_Functions.html#ext"><span class="std std-numref">Example 8.3.2</span></a>.</p>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Prove that
<span class="math notranslate nohighlight">\(\{x:\mathbb{Z} \mid x\text{ is odd}\}= \{a:\mathbb{Z} \mid \exists k:\mathbb{Z}, a = 2k - 1\}\)</span>.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>Let <span class="math notranslate nohighlight">\(x\)</span> be an integer. We must show that <span class="math notranslate nohighlight">\(x\)</span> is odd if and only if there exists an
integer <span class="math notranslate nohighlight">\(k\)</span> such that <span class="math notranslate nohighlight">\(x=2k-1\)</span>.</p>
<p>First, suppose that <span class="math notranslate nohighlight">\(x\)</span> is odd.  Then there exists an integer
<span class="math notranslate nohighlight">\(l\)</span> such that <span class="math notranslate nohighlight">\(x=2l+1\)</span>.  So</p>
<div class="math notranslate nohighlight">
\[\begin{split}x&amp;=2l+1\\
&amp;=2(l+1)-1.\end{split}\]</div>
<p>Conversely, suppose that there exists an integer <span class="math notranslate nohighlight">\(k\)</span> such that <span class="math notranslate nohighlight">\(x=2k-1\)</span>.  Then</p>
<div class="math notranslate nohighlight">
\[\begin{split}x&amp;=2k-1\\
&amp;=2(k-1)+1,\end{split}\]</div>
<p>so <span class="math notranslate nohighlight">\(x\)</span> is odd.</p>
</div>
<p>In Lean, as usual, we invoke an extensionality property using the tactic <code class="docutils literal notranslate"><span class="pre">ext</span></code>.  After unfolding
the definitions, the goal displays as</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="bp">&#8866;</span> <span class="n">Int.Odd</span> <span class="n">x</span> <span class="bp">&#8596;</span> <span class="bp">&#8707;</span> <span class="n">k</span><span class="o">,</span> <span class="n">x</span> <span class="bp">=</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">k</span> <span class="bp">-</span> <span class="mi">1</span>
</pre></div>
</div>
<p>This is the reformulation of the problem which we had stated in the first paragraph of the text proof.</p>
<p>Here is the full proof in Lean.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="o">{</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="n">Int.Odd</span> <span class="n">x</span><span class="o">}</span> <span class="bp">=</span> <span class="o">{</span><span class="n">a</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="bp">&#8707;</span> <span class="n">k</span><span class="o">,</span> <span class="n">a</span> <span class="bp">=</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">k</span> <span class="bp">-</span> <span class="mi">1</span><span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">ext</span> <span class="n">x</span>
  <span class="n">dsimp</span>
  <span class="n">constructor</span>
  <span class="bp">&#183;</span> <span class="n">intro</span> <span class="n">h</span>
    <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">l</span><span class="o">,</span> <span class="n">hl</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">h</span>
    <span class="n">use</span> <span class="n">l</span> <span class="bp">+</span> <span class="mi">1</span>
    <span class="k">calc</span> <span class="n">x</span> <span class="bp">=</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">l</span> <span class="bp">+</span> <span class="mi">1</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">hl</span><span class="o">]</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="mi">2</span> <span class="bp">*</span> <span class="o">(</span><span class="n">l</span> <span class="bp">+</span> <span class="mi">1</span><span class="o">)</span> <span class="bp">-</span> <span class="mi">1</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
  <span class="bp">&#183;</span> <span class="n">intro</span> <span class="n">h</span>
    <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">k</span><span class="o">,</span> <span class="n">hk</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">h</span>
    <span class="n">use</span> <span class="n">k</span> <span class="bp">-</span> <span class="mi">1</span>
    <span class="k">calc</span> <span class="n">x</span> <span class="bp">=</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">k</span> <span class="bp">-</span> <span class="mi">1</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">hk</span><span class="o">]</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="mi">2</span> <span class="bp">*</span> <span class="o">(</span><span class="n">k</span> <span class="bp">-</span> <span class="mi">1</span><span class="o">)</span> <span class="bp">+</span> <span class="mi">1</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
</pre></div>
</div>
</section>
<section id="id6">
<h3><span class="section-number">9.1.6. </span>Example<a class="headerlink" href="#id6" title="Permalink to this headline">&#61633;</a></h3>
<p>And to show that two sets are not equal in Lean, we produce an element of one which is not an
element of the other.</p>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Show that <span class="math notranslate nohighlight">\(\{a:\mathbb{N} \mid 4\mid a\}\ne\{b:\mathbb{N} \mid 2\mid b\}\)</span>.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>We will show that there exists a natural number <span class="math notranslate nohighlight">\(x\)</span> such that <span class="math notranslate nohighlight">\(2\mid x\)</span> and
<span class="math notranslate nohighlight">\(4\not\mid 6\)</span>.</p>
<p>Indeed, let us show that <span class="math notranslate nohighlight">\(6\)</span> has this property.  We have that <span class="math notranslate nohighlight">\(6=2\cdot 3\)</span>, so
<span class="math notranslate nohighlight">\(2\mid 6\)</span>, and <span class="math notranslate nohighlight">\(4\cdot 1 &lt; 6 &lt; 4 \cdot 2\)</span>, so <span class="math notranslate nohighlight">\(4\not\mid 6\)</span>.</p>
</div>
<p>In Lean, after applying set extensionality, unfolding the definitions and negation-normalizing, the
goal state shows as</p>
<div class="highlight-text notranslate"><div class="highlight"><pre><span></span>&#8866; &#8707; x, 4 &#8739; x &#8743; &#172;2 &#8739; x &#8744; &#172;4 &#8739; x &#8743; 2 &#8739; x
</pre></div>
</div>
<p>At this point we indicate our witness, 6, and specify that we will prove the right alternative,
<code class="docutils literal notranslate"><span class="pre">&#172;4</span> <span class="pre">&#8739;</span> <span class="pre">6</span> <span class="pre">&#8743;</span> <span class="pre">2</span> <span class="pre">&#8739;</span> <span class="pre">6</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="o">{</span><span class="n">a</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">|</span> <span class="mi">4</span> <span class="bp">&#8739;</span> <span class="n">a</span><span class="o">}</span> <span class="bp">&#8800;</span> <span class="o">{</span><span class="n">b</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">|</span> <span class="mi">2</span> <span class="bp">&#8739;</span> <span class="n">b</span><span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">ext</span>
  <span class="n">dsimp</span>
  <span class="n">push_neg</span>
  <span class="n">use</span> <span class="mi">6</span>
  <span class="n">right</span>
  <span class="n">constructor</span>
  <span class="bp">&#183;</span> <span class="n">apply</span> <span class="n">Nat.not_dvd_of_exists_lt_and_lt</span>
    <span class="n">use</span> <span class="mi">1</span>
    <span class="n">constructor</span> <span class="bp">&lt;;&gt;</span> <span class="n">numbers</span>
  <span class="bp">&#183;</span> <span class="n">use</span> <span class="mi">3</span>
    <span class="n">numbers</span>
</pre></div>
</div>
</section>
<section id="id7">
<h3><span class="section-number">9.1.7. </span>Example<a class="headerlink" href="#id7" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Prove or disprove that <span class="math notranslate nohighlight">\(\{k:\mathbb{Z} \mid 8\mid 5k\}=\{l:\mathbb{Z} \mid 8\mid l\}\)</span>.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>The statement is true.</p>
<p>Let <span class="math notranslate nohighlight">\(n\)</span> be an integer. We will show that <span class="math notranslate nohighlight">\(5n\)</span> is a multiple of 8 if and only if
<span class="math notranslate nohighlight">\(n\)</span> is.</p>
<p>First, suppose that <span class="math notranslate nohighlight">\(8\mid 5n\)</span>. Then there exists an integer <span class="math notranslate nohighlight">\(a\)</span> such that
<span class="math notranslate nohighlight">\(5n=8a\)</span>. So</p>
<div class="math notranslate nohighlight">
\[\begin{split}n &amp;= -3  (5  n) + 16 n \\
&amp;= -3  (8  a) + 16  n \\
&amp; = 8 (-3 a + 2  n),\end{split}\]</div>
<p>so <span class="math notranslate nohighlight">\(8\mid n\)</span>.</p>
<p>Conversely, suppose that <span class="math notranslate nohighlight">\(8\mid n\)</span>. Then there exists an integer <span class="math notranslate nohighlight">\(a\)</span> such that
<span class="math notranslate nohighlight">\(n=8a\)</span>. So</p>
<div class="math notranslate nohighlight">
\[\begin{split}5n &amp;= 5(8a) \\
&amp;= 8(5a),\end{split}\]</div>
<p>so <span class="math notranslate nohighlight">\(8\mid 5n\)</span>.</p>
</div>
<p>This problem turned out to be a disguised version of <a class="reference internal" href="04_Proofs_with_Structure_II.html#bezout-iff"><span class="std std-numref">Example 4.2.2</span></a>!</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="o">{</span><span class="n">k</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="mi">8</span> <span class="bp">&#8739;</span> <span class="mi">5</span> <span class="bp">*</span> <span class="n">k</span><span class="o">}</span> <span class="bp">=</span> <span class="o">{</span><span class="n">l</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="mi">8</span> <span class="bp">&#8739;</span> <span class="n">l</span><span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">ext</span> <span class="n">n</span>
  <span class="n">dsimp</span>
  <span class="n">constructor</span>
  <span class="bp">&#183;</span> <span class="n">intro</span> <span class="n">hn</span>
    <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">a</span><span class="o">,</span> <span class="n">ha</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">hn</span>
    <span class="n">use</span> <span class="bp">-</span><span class="mi">3</span> <span class="bp">*</span> <span class="n">a</span> <span class="bp">+</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">n</span>
    <span class="k">calc</span>
      <span class="n">n</span> <span class="bp">=</span> <span class="bp">-</span><span class="mi">3</span> <span class="bp">*</span> <span class="o">(</span><span class="mi">5</span> <span class="bp">*</span> <span class="n">n</span><span class="o">)</span> <span class="bp">+</span> <span class="mi">16</span> <span class="bp">*</span> <span class="n">n</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="bp">-</span><span class="mi">3</span> <span class="bp">*</span> <span class="o">(</span><span class="mi">8</span> <span class="bp">*</span> <span class="n">a</span><span class="o">)</span> <span class="bp">+</span> <span class="mi">16</span> <span class="bp">*</span> <span class="n">n</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">ha</span><span class="o">]</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="mi">8</span> <span class="bp">*</span> <span class="o">(</span><span class="bp">-</span><span class="mi">3</span> <span class="bp">*</span> <span class="n">a</span> <span class="bp">+</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">n</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
  <span class="bp">&#183;</span> <span class="n">intro</span> <span class="n">hn</span>
    <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">a</span><span class="o">,</span> <span class="n">ha</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">hn</span>
    <span class="n">use</span> <span class="mi">5</span> <span class="bp">*</span> <span class="n">a</span>
    <span class="k">calc</span> <span class="mi">5</span> <span class="bp">*</span> <span class="n">n</span> <span class="bp">=</span> <span class="mi">5</span> <span class="bp">*</span> <span class="o">(</span><span class="mi">8</span> <span class="bp">*</span> <span class="n">a</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">ha</span><span class="o">]</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="mi">8</span> <span class="bp">*</span> <span class="o">(</span><span class="mi">5</span> <span class="bp">*</span> <span class="n">a</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
</pre></div>
</div>
</section>
<section id="id8">
<h3><span class="section-number">9.1.8. </span>Example<a class="headerlink" href="#id8" title="Permalink to this headline">&#61633;</a></h3>
<p>There is a special notation <span class="math notranslate nohighlight">\(\{1,2,3\}\)</span> to refer to a finite set whose only elements are those
listed, here 1, 2 and 3.  By definition, <span class="math notranslate nohighlight">\(\{1,2,3\}\)</span> means
<span class="math notranslate nohighlight">\(\{x \mid x = 1 \lor x = 2 \lor x = 3\}\)</span>.  (The type, like <span class="math notranslate nohighlight">\(\mathbb{N}\)</span> or
<span class="math notranslate nohighlight">\(\mathbb{R}\)</span>, is usually inferred from context.)</p>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Prove  that <span class="math notranslate nohighlight">\(\{x:\mathbb{R} \mid x^2-x-2=0\}=\{-1, 2\}\)</span>.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>Let <span class="math notranslate nohighlight">\(x\)</span> be a real number. We must show that <span class="math notranslate nohighlight">\(x ^ 2 - x - 2 = 0\)</span> if and only if
<span class="math notranslate nohighlight">\(x=-1\)</span> or <span class="math notranslate nohighlight">\(x=2\)</span>.</p>
<p>First, suppose that <span class="math notranslate nohighlight">\(x ^ 2 - x - 2 = 0\)</span>.  Then</p>
<div class="math notranslate nohighlight">
\[\begin{split}(x+1)(x-2)&amp;=x ^ 2 - x - 2\\
&amp;=0,\end{split}\]</div>
<p>so either <span class="math notranslate nohighlight">\(x+1=0\)</span> or <span class="math notranslate nohighlight">\(x-2=0\)</span>.  If the former, <span class="math notranslate nohighlight">\(x=-1\)</span>. If the latter,
<span class="math notranslate nohighlight">\(x=2\)</span>.</p>
<p>Conversely, suppose that  <span class="math notranslate nohighlight">\(x=-1\)</span> or <span class="math notranslate nohighlight">\(x=2\)</span>.</p>
<p><strong>Case 1</strong> (<span class="math notranslate nohighlight">\(x=-1\)</span>): Then</p>
<div class="math notranslate nohighlight">
\[\begin{split}x^2-x-2&amp;=(-1)^2-(-1)-2\\
&amp;=0.\end{split}\]</div>
<p><strong>Case 1</strong> (<span class="math notranslate nohighlight">\(x=2\)</span>): Then</p>
<div class="math notranslate nohighlight">
\[\begin{split}x^2-x-2&amp;=2^2-2-2\\
&amp;=0.\end{split}\]</div>
</div>
<p>In Lean, after applying set extensionality and unfolding the definitions, the goal is</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="n">x</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">-</span> <span class="n">x</span> <span class="bp">-</span> <span class="mi">2</span> <span class="bp">=</span> <span class="mi">0</span> <span class="bp">&#8596;</span> <span class="n">x</span> <span class="bp">=</span> <span class="bp">-</span><span class="mi">1</span> <span class="bp">&#8744;</span> <span class="n">x</span> <span class="bp">=</span> <span class="mi">2</span>
</pre></div>
</div>
<p>and we start the written proof by explaining this.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="o">{</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8477;</span> <span class="bp">|</span> <span class="n">x</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">-</span> <span class="n">x</span> <span class="bp">-</span> <span class="mi">2</span> <span class="bp">=</span> <span class="mi">0</span><span class="o">}</span> <span class="bp">=</span> <span class="o">{</span><span class="bp">-</span><span class="mi">1</span><span class="o">,</span> <span class="mi">2</span><span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">ext</span> <span class="n">x</span>
  <span class="n">dsimp</span>
  <span class="n">constructor</span>
  <span class="bp">&#183;</span> <span class="n">intro</span> <span class="n">h</span>
    <span class="k">have</span> <span class="n">hx</span> <span class="o">:=</span>
    <span class="k">calc</span>
      <span class="o">(</span><span class="n">x</span> <span class="bp">+</span> <span class="mi">1</span><span class="o">)</span> <span class="bp">*</span> <span class="o">(</span><span class="n">x</span> <span class="bp">-</span> <span class="mi">2</span><span class="o">)</span> <span class="bp">=</span> <span class="n">x</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">-</span> <span class="n">x</span> <span class="bp">-</span> <span class="mi">2</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
        <span class="n">_</span> <span class="bp">=</span> <span class="mi">0</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">h</span><span class="o">]</span>
    <span class="n">rw</span> <span class="o">[</span><span class="n">mul_eq_zero</span><span class="o">]</span> <span class="n">at</span> <span class="n">hx</span>
    <span class="n">obtain</span> <span class="n">hx</span> <span class="bp">|</span> <span class="n">hx</span> <span class="o">:=</span> <span class="n">hx</span>
    <span class="bp">&#183;</span> <span class="n">left</span>
      <span class="n">addarith</span> <span class="o">[</span><span class="n">hx</span><span class="o">]</span>
    <span class="bp">&#183;</span> <span class="n">right</span>
      <span class="n">addarith</span> <span class="o">[</span><span class="n">hx</span><span class="o">]</span>
  <span class="bp">&#183;</span> <span class="n">intro</span> <span class="n">h</span>
    <span class="n">obtain</span> <span class="n">h</span> <span class="bp">|</span> <span class="n">h</span> <span class="o">:=</span> <span class="n">h</span>
    <span class="bp">&#183;</span> <span class="k">calc</span> <span class="n">x</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">-</span> <span class="n">x</span> <span class="bp">-</span> <span class="mi">2</span> <span class="bp">=</span> <span class="o">(</span><span class="bp">-</span><span class="mi">1</span><span class="o">)</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">-</span> <span class="o">(</span><span class="bp">-</span><span class="mi">1</span><span class="o">)</span> <span class="bp">-</span> <span class="mi">2</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">h</span><span class="o">]</span>
        <span class="n">_</span> <span class="bp">=</span> <span class="mi">0</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">numbers</span>
    <span class="bp">&#183;</span> <span class="k">calc</span> <span class="n">x</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">-</span> <span class="n">x</span> <span class="bp">-</span> <span class="mi">2</span> <span class="bp">=</span> <span class="mi">2</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">-</span> <span class="mi">2</span> <span class="bp">-</span> <span class="mi">2</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">h</span><span class="o">]</span>
        <span class="n">_</span> <span class="bp">=</span> <span class="mi">0</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">numbers</span>
</pre></div>
</div>
</section>
<section id="id9">
<h3><span class="section-number">9.1.9. </span>Example<a class="headerlink" href="#id9" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Prove  that <span class="math notranslate nohighlight">\(\{1,3,6\} \subseteq\{x:\mathbb{Q} \mid t&lt;10\}\)</span>.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>We must show that for all real numbers <span class="math notranslate nohighlight">\(t\)</span>, if <span class="math notranslate nohighlight">\(t=1\)</span> or <span class="math notranslate nohighlight">\(t=3\)</span> or <span class="math notranslate nohighlight">\(t=6\)</span>
then <span class="math notranslate nohighlight">\(t&lt;10\)</span>.  Indeed, <span class="math notranslate nohighlight">\(1&lt;10\)</span>, <span class="math notranslate nohighlight">\(3&lt;10\)</span> and <span class="math notranslate nohighlight">\(6&lt;10\)</span>.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="o">{</span><span class="mi">1</span><span class="o">,</span> <span class="mi">3</span><span class="o">,</span> <span class="mi">6</span><span class="o">}</span> <span class="bp">&#8838;</span> <span class="o">{</span><span class="n">t</span> <span class="o">:</span> <span class="n">&#8474;</span> <span class="bp">|</span> <span class="n">t</span> <span class="bp">&lt;</span> <span class="mi">10</span><span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Set.subset_def</span><span class="o">]</span>
  <span class="n">intro</span> <span class="n">t</span> <span class="n">ht</span>
  <span class="n">obtain</span> <span class="n">h1</span> <span class="bp">|</span> <span class="n">h3</span> <span class="bp">|</span> <span class="n">h6</span> <span class="o">:=</span> <span class="n">ht</span>
  <span class="bp">&#183;</span> <span class="n">addarith</span> <span class="o">[</span><span class="n">h1</span><span class="o">]</span>
  <span class="bp">&#183;</span> <span class="n">addarith</span> <span class="o">[</span><span class="n">h3</span><span class="o">]</span>
  <span class="bp">&#183;</span> <span class="n">addarith</span> <span class="o">[</span><span class="n">h6</span><span class="o">]</span>
</pre></div>
</div>
</section>
<section id="exercises">
<h3><span class="section-number">9.1.10. </span>Exercises<a class="headerlink" href="#exercises" title="Permalink to this headline">&#61633;</a></h3>
<ol class="arabic">
<li><p>Prove or disprove that <span class="math notranslate nohighlight">\(4\in \{a:\mathbb{Q} \mid a&lt;3\}\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="mi">4</span> <span class="bp">&#8712;</span> <span class="o">{</span><span class="n">a</span> <span class="o">:</span> <span class="n">&#8474;</span> <span class="bp">|</span> <span class="n">a</span> <span class="bp">&lt;</span> <span class="mi">3</span><span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="mi">4</span> <span class="bp">&#8713;</span> <span class="o">{</span><span class="n">a</span> <span class="o">:</span> <span class="n">&#8474;</span> <span class="bp">|</span> <span class="n">a</span> <span class="bp">&lt;</span> <span class="mi">3</span><span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Prove or disprove that <span class="math notranslate nohighlight">\(6\in \{n:\mathbb{N} \mid n\mid 42\}\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="mi">6</span> <span class="bp">&#8712;</span> <span class="o">{</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">|</span> <span class="n">n</span> <span class="bp">&#8739;</span> <span class="mi">42</span><span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="mi">6</span> <span class="bp">&#8713;</span> <span class="o">{</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">|</span> <span class="n">n</span> <span class="bp">&#8739;</span> <span class="mi">42</span><span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Prove or disprove that <span class="math notranslate nohighlight">\(8\in \{k:\mathbb{Z} \mid 5\mid k\}\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="mi">8</span> <span class="bp">&#8712;</span> <span class="o">{</span><span class="n">k</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="mi">5</span> <span class="bp">&#8739;</span> <span class="n">k</span><span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="mi">8</span> <span class="bp">&#8713;</span> <span class="o">{</span><span class="n">k</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="mi">5</span> <span class="bp">&#8739;</span> <span class="n">k</span><span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Prove or disprove that <span class="math notranslate nohighlight">\(11\in \{n:\mathbb{N} \mid n\text{ is odd}\}\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="mi">11</span> <span class="bp">&#8712;</span> <span class="o">{</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">|</span> <span class="n">Odd</span> <span class="n">n</span><span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="mi">11</span> <span class="bp">&#8713;</span> <span class="o">{</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">|</span> <span class="n">Odd</span> <span class="n">n</span><span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Prove or disprove that <span class="math notranslate nohighlight">\(-3\in \{x:\mathbb{R} \mid \forall y :\mathbb{R}, x\le y^2\}\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">-</span><span class="mi">3</span> <span class="bp">&#8712;</span> <span class="o">{</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8477;</span> <span class="bp">|</span> <span class="bp">&#8704;</span> <span class="n">y</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">,</span> <span class="n">x</span> <span class="bp">&#8804;</span> <span class="n">y</span> <span class="bp">^</span> <span class="mi">2</span><span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="bp">-</span><span class="mi">3</span> <span class="bp">&#8713;</span> <span class="o">{</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8477;</span> <span class="bp">|</span> <span class="bp">&#8704;</span> <span class="n">y</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">,</span> <span class="n">x</span> <span class="bp">&#8804;</span> <span class="n">y</span> <span class="bp">^</span> <span class="mi">2</span><span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Prove or disprove that
<span class="math notranslate nohighlight">\(\{a:\mathbb{N} \mid 20\mid a\}\subseteq \{x:\mathbb{N} \mid 5 \mid x\}\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="o">{</span><span class="n">a</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">|</span> <span class="mi">20</span> <span class="bp">&#8739;</span> <span class="n">a</span><span class="o">}</span> <span class="bp">&#8838;</span> <span class="o">{</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">|</span> <span class="mi">5</span> <span class="bp">&#8739;</span> <span class="n">x</span><span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="o">{</span><span class="n">a</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">|</span> <span class="mi">20</span> <span class="bp">&#8739;</span> <span class="n">a</span><span class="o">}</span> <span class="bp">&#8840;</span> <span class="o">{</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">|</span> <span class="mi">5</span> <span class="bp">&#8739;</span> <span class="n">x</span><span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Prove or disprove that
<span class="math notranslate nohighlight">\(\{a:\mathbb{N} \mid 5\mid a\}\subseteq \{x:\mathbb{N} \mid 20 \mid x\}\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="o">{</span><span class="n">a</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">|</span> <span class="mi">5</span> <span class="bp">&#8739;</span> <span class="n">a</span><span class="o">}</span> <span class="bp">&#8838;</span> <span class="o">{</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">|</span> <span class="mi">20</span> <span class="bp">&#8739;</span> <span class="n">x</span><span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="o">{</span><span class="n">a</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">|</span> <span class="mi">5</span> <span class="bp">&#8739;</span> <span class="n">a</span><span class="o">}</span> <span class="bp">&#8840;</span> <span class="o">{</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">|</span> <span class="mi">20</span> <span class="bp">&#8739;</span> <span class="n">x</span><span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Prove or disprove that
<span class="math notranslate nohighlight">\(\{r:\mathbb{Z} \mid 3\mid r\}\subseteq \{s:\mathbb{Z} \mid 0 \le s\}\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="o">{</span><span class="n">r</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="mi">3</span> <span class="bp">&#8739;</span> <span class="n">r</span><span class="o">}</span> <span class="bp">&#8838;</span> <span class="o">{</span><span class="n">s</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="mi">0</span> <span class="bp">&#8804;</span> <span class="n">s</span><span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="o">{</span><span class="n">r</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="mi">3</span> <span class="bp">&#8739;</span> <span class="n">r</span><span class="o">}</span> <span class="bp">&#8840;</span> <span class="o">{</span><span class="n">s</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="mi">0</span> <span class="bp">&#8804;</span> <span class="n">s</span><span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Prove or disprove that
<span class="math notranslate nohighlight">\(\{m:\mathbb{Z} \mid m\ge 10\}\subseteq \{n:\mathbb{Z} \mid n^3-7n^2\geq 4n\}\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="o">{</span><span class="n">m</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="n">m</span> <span class="bp">&#8805;</span> <span class="mi">10</span><span class="o">}</span> <span class="bp">&#8838;</span> <span class="o">{</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="n">n</span> <span class="bp">^</span> <span class="mi">3</span> <span class="bp">-</span> <span class="mi">7</span> <span class="bp">*</span> <span class="n">n</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">&#8805;</span> <span class="mi">4</span> <span class="bp">*</span> <span class="n">n</span><span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="o">{</span><span class="n">m</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="n">m</span> <span class="bp">&#8805;</span> <span class="mi">10</span><span class="o">}</span> <span class="bp">&#8840;</span> <span class="o">{</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="n">n</span> <span class="bp">^</span> <span class="mi">3</span> <span class="bp">-</span> <span class="mi">7</span> <span class="bp">*</span> <span class="n">n</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">&#8805;</span> <span class="mi">4</span> <span class="bp">*</span> <span class="n">n</span><span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Prove or disprove that
<span class="math notranslate nohighlight">\(\{n:\mathbb{Z} n\mid\text{ is even}\}=\{a:\mathbb{Z} \mid a\equiv 6\mod 2\}\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="o">{</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="n">Even</span> <span class="n">n</span><span class="o">}</span> <span class="bp">=</span> <span class="o">{</span><span class="n">a</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="n">a</span> <span class="bp">&#8801;</span> <span class="mi">6</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">2</span><span class="o">]}</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="o">{</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="n">Even</span> <span class="n">n</span><span class="o">}</span> <span class="bp">&#8800;</span> <span class="o">{</span><span class="n">a</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="n">a</span> <span class="bp">&#8801;</span> <span class="mi">6</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">2</span><span class="o">]}</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Prove or disprove that
<span class="math notranslate nohighlight">\(\{t:\mathbb{R} \mid t^2-5t+4=0\}=\{4\}\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="o">{</span><span class="n">t</span> <span class="o">:</span> <span class="n">&#8477;</span> <span class="bp">|</span> <span class="n">t</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">-</span> <span class="mi">5</span> <span class="bp">*</span> <span class="n">t</span> <span class="bp">+</span> <span class="mi">4</span> <span class="bp">=</span> <span class="mi">0</span><span class="o">}</span> <span class="bp">=</span> <span class="o">{</span><span class="mi">4</span><span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="o">{</span><span class="n">t</span> <span class="o">:</span> <span class="n">&#8477;</span> <span class="bp">|</span> <span class="n">t</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">-</span> <span class="mi">5</span> <span class="bp">*</span> <span class="n">t</span> <span class="bp">+</span> <span class="mi">4</span> <span class="bp">=</span> <span class="mi">0</span><span class="o">}</span> <span class="bp">&#8800;</span> <span class="o">{</span><span class="mi">4</span><span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Prove or disprove that <span class="math notranslate nohighlight">\(\{k:\mathbb{Z} \mid 8\mid 6k\}=\{l:\mathbb{Z} \mid 8\mid l\}\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="o">{</span><span class="n">k</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="mi">8</span> <span class="bp">&#8739;</span> <span class="mi">6</span> <span class="bp">*</span> <span class="n">k</span><span class="o">}</span> <span class="bp">=</span> <span class="o">{</span><span class="n">l</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="mi">8</span> <span class="bp">&#8739;</span> <span class="n">l</span><span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="o">{</span><span class="n">k</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="mi">8</span> <span class="bp">&#8739;</span> <span class="mi">6</span> <span class="bp">*</span> <span class="n">k</span><span class="o">}</span> <span class="bp">&#8800;</span> <span class="o">{</span><span class="n">l</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="mi">8</span> <span class="bp">&#8739;</span> <span class="n">l</span><span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Prove or disprove that <span class="math notranslate nohighlight">\(\{k:\mathbb{Z} \mid 7\mid 9k\}=\{l:\mathbb{Z} \mid 7\mid l\}\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="o">{</span><span class="n">k</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="mi">7</span> <span class="bp">&#8739;</span> <span class="mi">9</span> <span class="bp">*</span> <span class="n">k</span><span class="o">}</span> <span class="bp">=</span> <span class="o">{</span><span class="n">l</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="mi">7</span> <span class="bp">&#8739;</span> <span class="n">l</span><span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="o">{</span><span class="n">k</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="mi">7</span> <span class="bp">&#8739;</span> <span class="mi">9</span> <span class="bp">*</span> <span class="n">k</span><span class="o">}</span> <span class="bp">&#8800;</span> <span class="o">{</span><span class="n">l</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="mi">7</span> <span class="bp">&#8739;</span> <span class="n">l</span><span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Prove or disprove that <span class="math notranslate nohighlight">\(\{1,2,3\}=\{1,2\}\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="o">{</span><span class="mi">1</span><span class="o">,</span> <span class="mi">2</span><span class="o">,</span> <span class="mi">3</span><span class="o">}</span> <span class="bp">=</span> <span class="o">{</span><span class="mi">1</span><span class="o">,</span> <span class="mi">2</span><span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="o">{</span><span class="mi">1</span><span class="o">,</span> <span class="mi">2</span><span class="o">,</span> <span class="mi">3</span><span class="o">}</span> <span class="bp">&#8800;</span> <span class="o">{</span><span class="mi">1</span><span class="o">,</span> <span class="mi">2</span><span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Prove  that <span class="math notranslate nohighlight">\(\{x:\mathbb{R} \mid x^2+3x+2=0\}=\{-1, -2\}\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="o">{</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8477;</span> <span class="bp">|</span> <span class="n">x</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="mi">3</span> <span class="bp">*</span> <span class="n">x</span> <span class="bp">+</span> <span class="mi">2</span> <span class="bp">=</span> <span class="mi">0</span><span class="o">}</span> <span class="bp">=</span> <span class="o">{</span><span class="bp">-</span><span class="mi">1</span><span class="o">,</span> <span class="bp">-</span><span class="mi">2</span><span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
</ol>
</section>
</section>
<section id="set-operations">
<span id="id10"></span><h2><span class="section-number">9.2. </span>Set operations<a class="headerlink" href="#set-operations" title="Permalink to this headline">&#61633;</a></h2>
<section id="union">
<span id="id11"></span><h3><span class="section-number">9.2.1. </span>Example<a class="headerlink" href="#union" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-definition admonition">
<p class="admonition-title">Definition</p>
<p>The <em>union</em> of two sets <span class="math notranslate nohighlight">\(U\)</span> and <span class="math notranslate nohighlight">\(V\)</span> in a type <span class="math notranslate nohighlight">\(X\)</span>, denoted <span class="math notranslate nohighlight">\(U \cup V\)</span>,
is <span class="math notranslate nohighlight">\(\{x : X \mid x \in U \lor x \in V\}\)</span>.</p>
</div>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Let <span class="math notranslate nohighlight">\(t\)</span> be a real number.  Show that
<span class="math notranslate nohighlight">\(t&#8712;\{x:\mathbb{R}\mid-1&lt;x\}\cup \{x:\mathbb{R}\mid x &lt; 1\}\)</span>.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>We must show that either <span class="math notranslate nohighlight">\(-1&lt;t\)</span> or <span class="math notranslate nohighlight">\(t&lt;1\)</span>.</p>
<p><strong>Case 1</strong> (<span class="math notranslate nohighlight">\(t\le 0\)</span>): Then <span class="math notranslate nohighlight">\(t&lt;1\)</span>.</p>
<p><strong>Case 2</strong> (<span class="math notranslate nohighlight">\(t&gt; 0\)</span>): Then <span class="math notranslate nohighlight">\(-1&lt;t\)</span>.</p>
</div>
<p>After unfolding the definitions in this problem, the goal is to show that</p>
<div class="highlight-text notranslate"><div class="highlight"><pre><span></span>&#8866; -1 &lt; t &#8744; t &lt; 1
</pre></div>
</div>
<p>Here is the full proof in Lean.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">(</span><span class="n">t</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">)</span> <span class="o">:</span> <span class="n">t</span> <span class="bp">&#8712;</span> <span class="o">{</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8477;</span> <span class="bp">|</span> <span class="bp">-</span><span class="mi">1</span> <span class="bp">&lt;</span> <span class="n">x</span><span class="o">}</span> <span class="bp">&#8746;</span> <span class="o">{</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8477;</span> <span class="bp">|</span> <span class="n">x</span> <span class="bp">&lt;</span> <span class="mi">1</span><span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span>
  <span class="n">obtain</span> <span class="n">h</span> <span class="bp">|</span> <span class="n">h</span> <span class="o">:=</span> <span class="n">le_or_lt</span> <span class="n">t</span> <span class="mi">0</span>
  <span class="bp">&#183;</span> <span class="n">right</span>
    <span class="n">addarith</span> <span class="o">[</span><span class="n">h</span><span class="o">]</span>
  <span class="bp">&#183;</span> <span class="n">left</span>
    <span class="n">addarith</span> <span class="o">[</span><span class="n">h</span><span class="o">]</span>
</pre></div>
</div>
</section>
<section id="id12">
<h3><span class="section-number">9.2.2. </span>Example<a class="headerlink" href="#id12" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Show that <span class="math notranslate nohighlight">\(\{1,2\}\cup\{2,4\}=\{1,2,4\}\)</span>.</p>
</div>
<p>After applying set extensionality and unfolding definitions in this problem, the goal state is</p>
<div class="highlight-text notranslate"><div class="highlight"><pre><span></span>n : &#8469;
&#8866; (n = 1 &#8744; n = 2) &#8744; n = 2 &#8744; n = 4 &#8596; n = 1 &#8744; n = 2 &#8744; n = 4
</pre></div>
</div>
<p>It&#8217;s possible to prove this directly &#8211; here&#8217;s how the start of such a proof would look.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="o">{</span><span class="mi">1</span><span class="o">,</span> <span class="mi">2</span><span class="o">}</span> <span class="bp">&#8746;</span> <span class="o">{</span><span class="mi">2</span><span class="o">,</span> <span class="mi">4</span><span class="o">}</span> <span class="bp">=</span> <span class="o">{</span><span class="mi">1</span><span class="o">,</span> <span class="mi">2</span><span class="o">,</span> <span class="mi">4</span><span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">ext</span> <span class="n">n</span>
  <span class="n">dsimp</span>
  <span class="n">constructor</span>
  <span class="bp">&#183;</span> <span class="n">intro</span> <span class="n">h</span>
    <span class="n">obtain</span> <span class="o">(</span><span class="n">h</span> <span class="bp">|</span> <span class="n">h</span><span class="o">)</span> <span class="bp">|</span> <span class="o">(</span><span class="n">h</span> <span class="bp">|</span> <span class="n">h</span><span class="o">)</span> <span class="o">:=</span> <span class="n">h</span>
    <span class="bp">&#183;</span> <span class="n">left</span>
      <span class="n">apply</span> <span class="n">h</span>
    <span class="bp">&#183;</span> <span class="n">right</span>
      <span class="n">left</span>
      <span class="n">apply</span> <span class="n">h</span>
  <span class="c1">-- and much, much more</span>
    <span class="bp">&#183;</span> <span class="gr">sorry</span>
    <span class="bp">&#183;</span> <span class="gr">sorry</span>
  <span class="bp">&#183;</span> <span class="gr">sorry</span>
</pre></div>
</div>
<p>But there&#8217;s a better way: this is pure propositional logic, the situation the tactic <code class="docutils literal notranslate"><span class="pre">exhaust</span></code> (see
<a class="reference internal" href="08_Functions.html#musketeer"><span class="std std-numref">Example 8.1.8</span></a>) was designed for.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="o">{</span><span class="mi">2</span><span class="o">,</span> <span class="mi">1</span><span class="o">}</span> <span class="bp">&#8746;</span> <span class="o">{</span><span class="mi">2</span><span class="o">,</span> <span class="mi">4</span><span class="o">}</span> <span class="bp">=</span> <span class="o">{</span><span class="mi">1</span><span class="o">,</span> <span class="mi">2</span><span class="o">,</span> <span class="mi">4</span><span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">ext</span> <span class="n">n</span>
  <span class="n">dsimp</span>
  <span class="n">exhaust</span>
</pre></div>
</div>
</section>
<section id="id13">
<h3><span class="section-number">9.2.3. </span>Example<a class="headerlink" href="#id13" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-definition admonition">
<p class="admonition-title">Definition</p>
<p>The <em>intersection</em> of two sets <span class="math notranslate nohighlight">\(U\)</span> and <span class="math notranslate nohighlight">\(V\)</span> in a type <span class="math notranslate nohighlight">\(X\)</span>, denoted
<span class="math notranslate nohighlight">\(U \cap V\)</span>,
is <span class="math notranslate nohighlight">\(\{x : X \mid x \in U \land x \in V\}\)</span>.</p>
</div>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Show that
<span class="math notranslate nohighlight">\(\{-2,3\}\cap \{x:\mathbb{Q}\mid x^2=9\}\subseteq \{a:\mathbb{Q}\mid 0&lt;a\}\)</span>.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>We will show that for all real numbers <span class="math notranslate nohighlight">\(t\)</span>, if <span class="math notranslate nohighlight">\(t\)</span> is -2 or 3 and <span class="math notranslate nohighlight">\(t^2=9\)</span> then
<span class="math notranslate nohighlight">\(0&lt;t\)</span>.</p>
<p>Indeed, let <span class="math notranslate nohighlight">\(t\)</span> be a real number and suppose that <span class="math notranslate nohighlight">\(t\)</span> is -2 or 3 and <span class="math notranslate nohighlight">\(t^2=9\)</span>.</p>
<p><strong>Case 1</strong> (<span class="math notranslate nohighlight">\(t=-2\)</span>): We then have that</p>
<div class="math notranslate nohighlight">
\[\begin{split}(-2)^2&amp;=t^2\\
&amp;=9,\end{split}\]</div>
<p>contradiction.</p>
<p><strong>Case 2</strong> (<span class="math notranslate nohighlight">\(t=3\)</span>): Then <span class="math notranslate nohighlight">\(0&lt;t\)</span> as desired.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="o">{</span><span class="bp">-</span><span class="mi">2</span><span class="o">,</span> <span class="mi">3</span><span class="o">}</span> <span class="bp">&#8745;</span> <span class="o">{</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8474;</span> <span class="bp">|</span> <span class="n">x</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">=</span> <span class="mi">9</span><span class="o">}</span> <span class="bp">&#8838;</span> <span class="o">{</span><span class="n">a</span> <span class="o">:</span> <span class="n">&#8474;</span> <span class="bp">|</span> <span class="mi">0</span> <span class="bp">&lt;</span> <span class="n">a</span><span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Set.subset_def</span><span class="o">]</span>
  <span class="n">intro</span> <span class="n">t</span> <span class="n">h</span>
  <span class="n">obtain</span> <span class="o">&#10216;(</span><span class="n">h1</span> <span class="bp">|</span> <span class="n">h1</span><span class="o">),</span> <span class="n">h2</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">h</span>
  <span class="bp">&#183;</span> <span class="k">have</span> <span class="o">:=</span>
    <span class="k">calc</span> <span class="o">(</span><span class="bp">-</span><span class="mi">2</span><span class="o">)</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">=</span> <span class="n">t</span> <span class="bp">^</span> <span class="mi">2</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">h1</span><span class="o">]</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="mi">9</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">h2</span><span class="o">]</span>
    <span class="n">numbers</span> <span class="n">at</span> <span class="n">this</span>
  <span class="bp">&#183;</span> <span class="n">addarith</span> <span class="o">[</span><span class="n">h1</span><span class="o">]</span>
</pre></div>
</div>
</section>
<section id="id14">
<h3><span class="section-number">9.2.4. </span>Example<a class="headerlink" href="#id14" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Show that
<span class="math notranslate nohighlight">\(\{n:\mathbb{N}\mid 4\le n\}\cap \{n:\mathbb{N}\mid n&lt;7\}\subseteq\{4,5,6\}\)</span>.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="o">{</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">|</span> <span class="mi">4</span> <span class="bp">&#8804;</span> <span class="n">n</span><span class="o">}</span> <span class="bp">&#8745;</span> <span class="o">{</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">|</span> <span class="n">n</span> <span class="bp">&lt;</span> <span class="mi">7</span><span class="o">}</span> <span class="bp">&#8838;</span> <span class="o">{</span><span class="mi">4</span><span class="o">,</span> <span class="mi">5</span><span class="o">,</span> <span class="mi">6</span><span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Set.subset_def</span><span class="o">]</span>
  <span class="n">intro</span> <span class="n">n</span> <span class="n">h</span>
  <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">h1</span><span class="o">,</span> <span class="n">h2</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">h</span>
  <span class="n">interval_cases</span> <span class="n">n</span> <span class="bp">&lt;;&gt;</span> <span class="n">exhaust</span>
</pre></div>
</div>
</section>
<section id="id15">
<h3><span class="section-number">9.2.5. </span>Example<a class="headerlink" href="#id15" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-definition admonition">
<p class="admonition-title">Definition</p>
<p>The <em>complement</em> of a set <span class="math notranslate nohighlight">\(U\)</span>  in a type <span class="math notranslate nohighlight">\(X\)</span>, denoted
<span class="math notranslate nohighlight">\(U^{c}\)</span>, is <span class="math notranslate nohighlight">\(\{x : X \mid x \notin U\}\)</span>.</p>
</div>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Show that
<span class="math notranslate nohighlight">\(\{n:\mathbb{Z}\mid n\text{ even}\}^{c}=\{n:\mathbb{N}\mid n\text{ odd}\}\)</span>.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>Let <span class="math notranslate nohighlight">\(n\)</span> be an integer. We must show that <span class="math notranslate nohighlight">\(n\)</span> is odd if and only if it is not even.
This is precisely <a class="reference internal" href="04_Proofs_with_Structure_II.html#even-iff-not-odd"><span class="std std-numref">Example 4.5.5</span></a>.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="o">{</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="n">Even</span> <span class="n">n</span><span class="o">}</span><span class="bp">&#7580;</span> <span class="bp">=</span> <span class="o">{</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="n">Odd</span> <span class="n">n</span><span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">ext</span> <span class="n">n</span>
  <span class="n">dsimp</span>
  <span class="n">rw</span> <span class="o">[</span><span class="n">odd_iff_not_even</span><span class="o">]</span>
</pre></div>
</div>
</section>
<section id="id16">
<h3><span class="section-number">9.2.6. </span>Example<a class="headerlink" href="#id16" title="Permalink to this headline">&#61633;</a></h3>
<p>The <em>empty set</em> in a type <span class="math notranslate nohighlight">\(X\)</span> is the set which has no elements.  That&#8217;s a slightly informal
description: here&#8217;s the strict definition.</p>
<div class="admonition-definition admonition">
<p class="admonition-title">Definition</p>
<p>The <em>empty set</em> in a type <span class="math notranslate nohighlight">\(X\)</span>, denoted <span class="math notranslate nohighlight">\(\emptyset\)</span>, is <span class="math notranslate nohighlight">\(\{x : X \mid \operatorname{False}\}\)</span>.</p>
</div>
<p>It is true by pure logic that no element of type <span class="math notranslate nohighlight">\(X\)</span> belongs to the empty set in <span class="math notranslate nohighlight">\(X\)</span>,
and that the empty set in <span class="math notranslate nohighlight">\(X\)</span> is a subset of every set in <span class="math notranslate nohighlight">\(X\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">(</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="o">:</span> <span class="n">x</span> <span class="bp">&#8713;</span> <span class="bp">&#8709;</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span>
  <span class="n">exhaust</span>

<span class="kd">example</span> <span class="o">(</span><span class="n">U</span> <span class="o">:</span> <span class="n">Set</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="o">:</span> <span class="bp">&#8709;</span> <span class="bp">&#8838;</span> <span class="n">U</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Set.subset_def</span><span class="o">]</span>
  <span class="n">intro</span> <span class="n">x</span>
  <span class="n">exhaust</span>
</pre></div>
</div>
<p>To show a set <span class="math notranslate nohighlight">\(U\)</span> in <span class="math notranslate nohighlight">\(X\)</span> is equal to the empty set, you must show that <span class="math notranslate nohighlight">\(U\)</span> has
no elements.</p>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Show that
<span class="math notranslate nohighlight">\(\{n:\mathbb{Z}\mid n\equiv 1\mod 5\}\cap\{n:\mathbb{N}\mid n\equiv 1\mod 5\}=\emptyset\)</span>.</p>
</div>
<p>Let&#8217;s consider the Lean proof first.  We can write something like this:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="o">{</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="n">n</span> <span class="bp">&#8801;</span> <span class="mi">1</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">5</span><span class="o">]}</span> <span class="bp">&#8745;</span> <span class="o">{</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="n">n</span> <span class="bp">&#8801;</span> <span class="mi">2</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">5</span><span class="o">]}</span> <span class="bp">=</span> <span class="bp">&#8709;</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">ext</span> <span class="n">x</span>
  <span class="n">dsimp</span>
  <span class="n">constructor</span>
  <span class="bp">&#183;</span> <span class="n">intro</span> <span class="n">hx</span>
    <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">hx1</span><span class="o">,</span> <span class="n">hx2</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">hx</span>
    <span class="k">have</span> <span class="o">:=</span>
    <span class="k">calc</span> <span class="mi">1</span> <span class="bp">&#8801;</span> <span class="n">x</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">5</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rel</span> <span class="o">[</span><span class="n">hx1</span><span class="o">]</span>
      <span class="n">_</span> <span class="bp">&#8801;</span> <span class="mi">2</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">5</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rel</span> <span class="o">[</span><span class="n">hx2</span><span class="o">]</span>
    <span class="n">numbers</span> <span class="n">at</span> <span class="n">this</span>
  <span class="bp">&#183;</span> <span class="n">intro</span> <span class="n">hx</span>
    <span class="n">contradiction</span>
</pre></div>
</div>
<p>But a certain amount of that proof (the <code class="docutils literal notranslate"><span class="pre">constructor</span></code>, and the <code class="docutils literal notranslate"><span class="pre">intro</span></code>/<code class="docutils literal notranslate"><span class="pre">contradiction</span></code> in the
second branch of the proof) is just logical messing-around.  Now that we are familiar with the full
power of the <code class="docutils literal notranslate"><span class="pre">exhaust</span></code> tactic it is possible to streamline proofs like this.  Have a look at the
goal state after the <code class="docutils literal notranslate"><span class="pre">dsimp</span></code>: it is</p>
<div class="highlight-text notranslate"><div class="highlight"><pre><span></span>&#8866; x &#8801; 1 [ZMOD 5] &#8743; x &#8801; 2 [ZMOD 5] &#8596; False
</pre></div>
</div>
<p>and you might mentally simplify this to the logically equivalent</p>
<div class="highlight-text notranslate"><div class="highlight"><pre><span></span>&#8866; &#172; (x &#8801; 1 [ZMOD 5] &#8743; x &#8801; 2 [ZMOD 5])
</pre></div>
</div>
<p>This reformulation can be carried out in Lean using the incantation</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">suffices</span> <span class="bp">&#172;</span><span class="o">(</span><span class="n">x</span> <span class="bp">&#8801;</span> <span class="mi">1</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">5</span><span class="o">]</span> <span class="bp">&#8743;</span> <span class="n">x</span> <span class="bp">&#8801;</span> <span class="mi">2</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">5</span><span class="o">])</span> <span class="kd">by</span> <span class="n">exhaust</span>
</pre></div>
</div>
<p>Here is a full proof in Lean using this approach.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="o">{</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="n">n</span> <span class="bp">&#8801;</span> <span class="mi">1</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">5</span><span class="o">]}</span> <span class="bp">&#8745;</span> <span class="o">{</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="n">n</span> <span class="bp">&#8801;</span> <span class="mi">2</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">5</span><span class="o">]}</span> <span class="bp">=</span> <span class="bp">&#8709;</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">ext</span> <span class="n">x</span>
  <span class="n">dsimp</span>
  <span class="k">suffices</span> <span class="bp">&#172;</span><span class="o">(</span><span class="n">x</span> <span class="bp">&#8801;</span> <span class="mi">1</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">5</span><span class="o">]</span> <span class="bp">&#8743;</span> <span class="n">x</span> <span class="bp">&#8801;</span> <span class="mi">2</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">5</span><span class="o">])</span> <span class="kd">by</span> <span class="n">exhaust</span>
  <span class="n">intro</span> <span class="n">hx</span>
  <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">hx1</span><span class="o">,</span> <span class="n">hx2</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">hx</span>
  <span class="k">have</span> <span class="o">:=</span>
  <span class="k">calc</span> <span class="mi">1</span> <span class="bp">&#8801;</span> <span class="n">x</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">5</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rel</span> <span class="o">[</span><span class="n">hx1</span><span class="o">]</span>
    <span class="n">_</span> <span class="bp">&#8801;</span> <span class="mi">2</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">5</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rel</span> <span class="o">[</span><span class="n">hx2</span><span class="o">]</span>
  <span class="n">numbers</span> <span class="n">at</span> <span class="n">this</span>
</pre></div>
</div>
<p>And here is that proof in words.  We combine the use of set extensionality, the
definition-unfolding, and the logically equivalent reformulation into a single paragraph of setup.</p>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>Let <span class="math notranslate nohighlight">\(x\)</span> be an integer.  We will show that it is not true that both
<span class="math notranslate nohighlight">\(x\equiv 1\mod 5\)</span> and <span class="math notranslate nohighlight">\(x\equiv 2\mod 5\)</span>.</p>
<p>Indeed, suppose that <span class="math notranslate nohighlight">\(x\equiv 1\mod 5\)</span> and <span class="math notranslate nohighlight">\(x\equiv 2\mod 5\)</span>.  Then</p>
<div class="math notranslate nohighlight">
\[\begin{split}1&amp;\equiv x\mod 5\\
&amp;\equiv 2\mod 5,\end{split}\]</div>
<p>contradiction.</p>
</div>
</section>
<section id="id17">
<h3><span class="section-number">9.2.7. </span>Example<a class="headerlink" href="#id17" title="Permalink to this headline">&#61633;</a></h3>
<p>The <em>universe set</em> in a type <span class="math notranslate nohighlight">\(X\)</span> is the set which contains everything in <span class="math notranslate nohighlight">\(X\)</span>.
That&#8217;s again a slightly informal description: here&#8217;s the strict definition.</p>
<div class="admonition-definition admonition">
<p class="admonition-title">Definition</p>
<p>The <em>universe set</em> in a type <span class="math notranslate nohighlight">\(X\)</span> is <span class="math notranslate nohighlight">\(\{x : X \mid \operatorname{True}\}\)</span>.</p>
</div>
<p>It is true by pure logic that all elements of type <span class="math notranslate nohighlight">\(X\)</span> belong to the universe set in
<span class="math notranslate nohighlight">\(X\)</span>, and that every set in <span class="math notranslate nohighlight">\(X\)</span> is a subset of the universe set in <span class="math notranslate nohighlight">\(X\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">(</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="o">:</span> <span class="n">x</span> <span class="bp">&#8712;</span> <span class="n">univ</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">dsimp</span>

<span class="kd">example</span> <span class="o">(</span><span class="n">U</span> <span class="o">:</span> <span class="n">Set</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="o">:</span> <span class="n">U</span> <span class="bp">&#8838;</span> <span class="n">univ</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Set.subset_def</span><span class="o">]</span>
  <span class="n">intro</span> <span class="n">x</span>
  <span class="n">exhaust</span>
</pre></div>
</div>
<p>Note that in Lean the universe set is denoted <code class="docutils literal notranslate"><span class="pre">univ</span></code>.  On paper we often refer to the universe
set of <span class="math notranslate nohighlight">\(X\)</span> as <span class="math notranslate nohighlight">\(X\)</span>, too (even though this is not strictly correct).</p>
<p>To show a set <span class="math notranslate nohighlight">\(U\)</span> in <span class="math notranslate nohighlight">\(X\)</span> is equal to the universe set, you must show that <span class="math notranslate nohighlight">\(U\)</span>
contains all elements of <span class="math notranslate nohighlight">\(X\)</span>.  Here we adapt <a class="reference internal" href="#union"><span class="std std-numref">Example 9.2.1</span></a> to be a problem about
the universe set.</p>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Show that <span class="math notranslate nohighlight">\(\{x:\mathbb{R}\mid-1&lt;x\}\cup \{x:\mathbb{R}\mid x &lt; 1\}=\mathbb{R}\)</span>.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>We must show that for all real numbers <span class="math notranslate nohighlight">\(t\)</span>, either <span class="math notranslate nohighlight">\(-1&lt;t\)</span> or <span class="math notranslate nohighlight">\(t&lt;1\)</span>.</p>
<p><strong>Case 1</strong> (<span class="math notranslate nohighlight">\(t\le 0\)</span>): Then <span class="math notranslate nohighlight">\(t&lt;1\)</span>.</p>
<p><strong>Case 2</strong> (<span class="math notranslate nohighlight">\(t&gt; 0\)</span>): Then <span class="math notranslate nohighlight">\(-1&lt;t\)</span>.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="o">{</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8477;</span> <span class="bp">|</span> <span class="bp">-</span><span class="mi">1</span> <span class="bp">&lt;</span> <span class="n">x</span><span class="o">}</span> <span class="bp">&#8746;</span> <span class="o">{</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8477;</span> <span class="bp">|</span> <span class="n">x</span> <span class="bp">&lt;</span> <span class="mi">1</span><span class="o">}</span> <span class="bp">=</span> <span class="n">univ</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">ext</span> <span class="n">t</span>
  <span class="n">dsimp</span>
  <span class="k">suffices</span> <span class="bp">-</span><span class="mi">1</span> <span class="bp">&lt;</span> <span class="n">t</span> <span class="bp">&#8744;</span> <span class="n">t</span> <span class="bp">&lt;</span> <span class="mi">1</span> <span class="kd">by</span> <span class="n">exhaust</span>
  <span class="n">obtain</span> <span class="n">h</span> <span class="bp">|</span> <span class="n">h</span> <span class="o">:=</span> <span class="n">le_or_lt</span> <span class="n">t</span> <span class="mi">0</span>
  <span class="bp">&#183;</span> <span class="n">right</span>
    <span class="n">addarith</span> <span class="o">[</span><span class="n">h</span><span class="o">]</span>
  <span class="bp">&#183;</span> <span class="n">left</span>
    <span class="n">addarith</span> <span class="o">[</span><span class="n">h</span><span class="o">]</span>
</pre></div>
</div>
</section>
<section id="id18">
<h3><span class="section-number">9.2.8. </span>Exercises<a class="headerlink" href="#id18" title="Permalink to this headline">&#61633;</a></h3>
<p>For the first five problems, I provide a tactic <code class="docutils literal notranslate"><span class="pre">check_equality_of_explicit_sets</span></code> which will prove
the statement if you have formulated it correctly.  This tactic simply runs <code class="docutils literal notranslate"><span class="pre">ext</span></code>, then <code class="docutils literal notranslate"><span class="pre">dsimp</span></code>,
then <code class="docutils literal notranslate"><span class="pre">exhaust</span></code>:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="n">macro</span> <span class="s2">&quot;check_equality_of_explicit_sets&quot;</span> <span class="o">:</span> <span class="n">tactic</span> <span class="bp">=&gt;</span> <span class="bp">`</span><span class="o">(</span><span class="n">tactic</span><span class="bp">|</span> <span class="o">(</span><span class="n">ext</span><span class="bp">;</span> <span class="n">dsimp</span><span class="bp">;</span> <span class="n">exhaust</span><span class="o">))</span>
</pre></div>
</div>
<ol class="arabic">
<li><p>Write in an explicitly-listed finite set without repeats, or <span class="math notranslate nohighlight">\(\emptyset\)</span>, which is equal
to <span class="math notranslate nohighlight">\(\{-1,2,4,4\}\cup\{3,-2,2\}\)</span>.  When you have the correct answer, the given Lean proof
will work.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="o">{</span><span class="bp">-</span><span class="mi">1</span><span class="o">,</span> <span class="mi">2</span><span class="o">,</span> <span class="mi">4</span><span class="o">,</span> <span class="mi">4</span><span class="o">}</span> <span class="bp">&#8746;</span> <span class="o">{</span><span class="mi">3</span><span class="o">,</span> <span class="bp">-</span><span class="mi">2</span><span class="o">,</span> <span class="mi">2</span><span class="o">}</span> <span class="bp">=</span> <span class="gr">sorry</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">check_equality_of_explicit_sets</span>
</pre></div>
</div>
</li>
<li><p>Write in an explicitly-listed finite set without repeats, or <span class="math notranslate nohighlight">\(\emptyset\)</span>, which is equal
to <span class="math notranslate nohighlight">\(\{-1,2,4,4\}\cup\{3,-2,2\}\)</span>.  When you have the correct answer, the given Lean proof
will work.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="o">{</span><span class="mi">0</span><span class="o">,</span> <span class="mi">1</span><span class="o">,</span> <span class="mi">2</span><span class="o">,</span> <span class="mi">3</span><span class="o">,</span> <span class="mi">4</span><span class="o">}</span> <span class="bp">&#8745;</span> <span class="o">{</span><span class="mi">0</span><span class="o">,</span> <span class="mi">2</span><span class="o">,</span> <span class="mi">4</span><span class="o">,</span> <span class="mi">6</span><span class="o">,</span> <span class="mi">8</span><span class="o">}</span> <span class="bp">=</span> <span class="gr">sorry</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">check_equality_of_explicit_sets</span>
</pre></div>
</div>
</li>
<li><p>Write in an explicitly-listed finite set without repeats, or <span class="math notranslate nohighlight">\(\emptyset\)</span>, which is equal
to <span class="math notranslate nohighlight">\(\{1,2\}\cap\{3\}\)</span>.  When you have the correct answer, the given Lean proof
will work.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="o">{</span><span class="mi">1</span><span class="o">,</span> <span class="mi">2</span><span class="o">}</span> <span class="bp">&#8745;</span> <span class="o">{</span><span class="mi">3</span><span class="o">}</span> <span class="bp">=</span> <span class="gr">sorry</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">check_equality_of_explicit_sets</span>
</pre></div>
</div>
</li>
<li><p>Write in an explicitly-listed finite set without repeats, or <span class="math notranslate nohighlight">\(\emptyset\)</span>, which is equal
to <span class="math notranslate nohighlight">\(\{3,4,5\}^c\cap\{1,3,5,7,9\}\)</span>.  When you have the correct answer, the given Lean proof
will work.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="o">{</span><span class="mi">3</span><span class="o">,</span> <span class="mi">4</span><span class="o">,</span> <span class="mi">5</span><span class="o">}</span><span class="bp">&#7580;</span> <span class="bp">&#8745;</span> <span class="o">{</span><span class="mi">1</span><span class="o">,</span> <span class="mi">3</span><span class="o">,</span> <span class="mi">5</span><span class="o">,</span> <span class="mi">7</span><span class="o">,</span> <span class="mi">9</span><span class="o">}</span> <span class="bp">=</span> <span class="gr">sorry</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">check_equality_of_explicit_sets</span>
</pre></div>
</div>
</li>
<li><p>Prove that
<span class="math notranslate nohighlight">\(\{r:\mathbb{Z}\mid r\equiv 7\mod 10\}\subseteq \{s:\mathbb{Z}\mid s\equiv 1\mod 2\}\cap\{t:\mathbb{Z}\mid t\equiv 2\mod 5\}\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="o">{</span><span class="n">r</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="n">r</span> <span class="bp">&#8801;</span> <span class="mi">7</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">10</span><span class="o">]</span> <span class="o">}</span>
    <span class="bp">&#8838;</span> <span class="o">{</span><span class="n">s</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="n">s</span> <span class="bp">&#8801;</span> <span class="mi">1</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">2</span><span class="o">]}</span> <span class="bp">&#8745;</span> <span class="o">{</span><span class="n">t</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="n">t</span> <span class="bp">&#8801;</span> <span class="mi">2</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">5</span><span class="o">]}</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Prove that
<span class="math notranslate nohighlight">\(\{n:\mathbb{Z}\mid 5\mid n\}\cap \{n:\mathbb{Z}\mid 8\mid n\}&#8838;\{n:\mathbb{Z}\mid 40\mid n\}\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="o">{</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="mi">5</span> <span class="bp">&#8739;</span> <span class="n">n</span><span class="o">}</span> <span class="bp">&#8745;</span> <span class="o">{</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="mi">8</span> <span class="bp">&#8739;</span> <span class="n">n</span><span class="o">}</span> <span class="bp">&#8838;</span> <span class="o">{</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="mi">40</span> <span class="bp">&#8739;</span> <span class="n">n</span><span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Prove that <span class="math notranslate nohighlight">\(\{n:\mathbb{Z}\mid 3\mid n\}\cup \{n:\mathbb{Z}\mid 2\mid n\}&#8838;\{n:\mathbb{Z}\mid n^2\equiv 1\mod 6\}^{c}\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span>
    <span class="o">{</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="mi">3</span> <span class="bp">&#8739;</span> <span class="n">n</span><span class="o">}</span> <span class="bp">&#8746;</span> <span class="o">{</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="mi">2</span> <span class="bp">&#8739;</span> <span class="n">n</span><span class="o">}</span> <span class="bp">&#8838;</span> <span class="o">{</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="n">n</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">&#8801;</span> <span class="mi">1</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">6</span><span class="o">]}</span><span class="bp">&#7580;</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Let us define that a set <span class="math notranslate nohighlight">\(s\)</span> in a type <span class="math notranslate nohighlight">\(X\)</span> has <em>size at least two</em>, if there exist
<span class="math notranslate nohighlight">\(x_1\)</span> and <span class="math notranslate nohighlight">\(x_2\)</span> in <span class="math notranslate nohighlight">\(s\)</span> which are different, and has <em>size at least
three</em>, if there exist <span class="math notranslate nohighlight">\(x_1\)</span>, <span class="math notranslate nohighlight">\(x_2\)</span> and <span class="math notranslate nohighlight">\(x_3\)</span> in <span class="math notranslate nohighlight">\(s\)</span> which are all
different.</p>
<p>Let <span class="math notranslate nohighlight">\(s\)</span> and <span class="math notranslate nohighlight">\(t\)</span> be sets of size at least two in some type <span class="math notranslate nohighlight">\(X\)</span>, and suppose
that <span class="math notranslate nohighlight">\(s \cap t\)</span> does not have size at least two.  Show that <span class="math notranslate nohighlight">\(s\cup t\)</span> has size at
least three.</p>
<p>This problem features a ton of different cases.  Use <code class="docutils literal notranslate"><span class="pre">exhaust</span></code> liberally to knock off sub-cases.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span> <span class="n">SizeAtLeastTwo</span> <span class="o">(</span><span class="n">s</span> <span class="o">:</span> <span class="n">Set</span> <span class="n">X</span><span class="o">)</span> <span class="o">:</span> <span class="kt">Prop</span> <span class="o">:=</span> <span class="bp">&#8707;</span> <span class="n">x1</span> <span class="n">x2</span> <span class="o">:</span> <span class="n">X</span><span class="o">,</span> <span class="n">x1</span> <span class="bp">&#8800;</span> <span class="n">x2</span> <span class="bp">&#8743;</span> <span class="n">x1</span> <span class="bp">&#8712;</span> <span class="n">s</span> <span class="bp">&#8743;</span> <span class="n">x2</span> <span class="bp">&#8712;</span> <span class="n">s</span>
<span class="kd">def</span> <span class="n">SizeAtLeastThree</span> <span class="o">(</span><span class="n">s</span> <span class="o">:</span> <span class="n">Set</span> <span class="n">X</span><span class="o">)</span> <span class="o">:</span> <span class="kt">Prop</span> <span class="o">:=</span>
  <span class="bp">&#8707;</span> <span class="n">x1</span> <span class="n">x2</span> <span class="n">x3</span> <span class="o">:</span> <span class="n">X</span><span class="o">,</span> <span class="n">x1</span> <span class="bp">&#8800;</span> <span class="n">x2</span> <span class="bp">&#8743;</span> <span class="n">x1</span> <span class="bp">&#8800;</span> <span class="n">x3</span> <span class="bp">&#8743;</span> <span class="n">x2</span> <span class="bp">&#8800;</span> <span class="n">x3</span> <span class="bp">&#8743;</span> <span class="n">x1</span> <span class="bp">&#8712;</span> <span class="n">s</span> <span class="bp">&#8743;</span> <span class="n">x2</span> <span class="bp">&#8712;</span> <span class="n">s</span> <span class="bp">&#8743;</span> <span class="n">x3</span> <span class="bp">&#8712;</span> <span class="n">s</span>

<span class="kd">example</span> <span class="o">{</span><span class="n">s</span> <span class="n">t</span> <span class="o">:</span> <span class="n">Set</span> <span class="n">X</span><span class="o">}</span> <span class="o">(</span><span class="n">hs</span> <span class="o">:</span> <span class="n">SizeAtLeastTwo</span> <span class="n">s</span><span class="o">)</span> <span class="o">(</span><span class="n">ht</span> <span class="o">:</span> <span class="n">SizeAtLeastTwo</span> <span class="n">t</span><span class="o">)</span>
    <span class="o">(</span><span class="n">hst</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">SizeAtLeastTwo</span> <span class="o">(</span><span class="n">s</span> <span class="bp">&#8745;</span> <span class="n">t</span><span class="o">))</span> <span class="o">:</span>
    <span class="n">SizeAtLeastThree</span> <span class="o">(</span><span class="n">s</span> <span class="bp">&#8746;</span> <span class="n">t</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
</ol>
</section>
</section>
<section id="the-type-of-sets">
<span id="powerset"></span><h2><span class="section-number">9.3. </span>The type of sets<a class="headerlink" href="#the-type-of-sets" title="Permalink to this headline">&#61633;</a></h2>
<section id="definition">
<h3><span class="section-number">9.3.1. </span>Definition<a class="headerlink" href="#definition" title="Permalink to this headline">&#61633;</a></h3>
<p>Let <span class="math notranslate nohighlight">\(X\)</span> be a type.  The collection of all sets in <span class="math notranslate nohighlight">\(X\)</span> can itself be
considered as a type.  This type is sometimes denoted <span class="math notranslate nohighlight">\(\mathcal{P}(X)\)</span>. <a class="footnote-reference brackets" href="#id25" id="id19">1</a>  For
example, <span class="math notranslate nohighlight">\(\{3,4,5\}\)</span>, <span class="math notranslate nohighlight">\(\{n:\mathbb{N}\mid 8&lt;n\}\)</span>, and
<span class="math notranslate nohighlight">\(\{k:\mathbb{N}\mid\exists \ a, a^2=k\}\)</span> are all sets of natural numbers, which
means they are all of type <span class="math notranslate nohighlight">\(\mathcal{P}(\mathbb{N})\)</span>.</p>
<p>In Lean, for a type <code class="docutils literal notranslate"><span class="pre">X</span></code>, the type of sets in <code class="docutils literal notranslate"><span class="pre">X</span></code> is denoted <code class="docutils literal notranslate"><span class="pre">Set</span> <span class="pre">X</span></code>.  Lean
will confirm that the three objects described above all have type <code class="docutils literal notranslate"><span class="pre">Set</span> <span class="pre">&#8469;</span></code>:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span> <span class="o">{</span><span class="mi">3</span><span class="o">,</span> <span class="mi">4</span><span class="o">,</span> <span class="mi">5</span><span class="o">}</span> <span class="c1">-- `{3, 4, 5} : Set &#8469;`</span>
<span class="k">#check</span> <span class="o">{</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">|</span> <span class="mi">8</span> <span class="bp">&lt;</span> <span class="n">n</span><span class="o">}</span> <span class="c1">-- `{n | 8 &lt; n} : Set &#8469;`</span>
<span class="k">#check</span> <span class="o">{</span><span class="n">k</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">|</span> <span class="bp">&#8707;</span> <span class="n">a</span><span class="o">,</span> <span class="n">a</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">=</span> <span class="n">k</span><span class="o">}</span> <span class="c1">-- `{k | &#8707; a, a ^ 2 = k} : Set &#8469;`</span>
</pre></div>
</div>
<p>This operation can be iterated: you can have sets in the type of sets, and so on.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span> <span class="o">{{</span><span class="mi">3</span><span class="o">,</span> <span class="mi">4</span><span class="o">},</span> <span class="o">{</span><span class="mi">4</span><span class="o">,</span> <span class="mi">5</span><span class="o">,</span> <span class="mi">6</span><span class="o">}}</span> <span class="c1">-- `{{3, 4}, {4, 5, 6}} : Set (Set &#8469;)`</span>
<span class="k">#check</span> <span class="o">{</span><span class="n">s</span> <span class="o">:</span> <span class="n">Set</span> <span class="n">&#8469;</span> <span class="bp">|</span> <span class="mi">3</span> <span class="bp">&#8712;</span> <span class="n">s</span><span class="o">}</span> <span class="c1">-- `{s | 3 &#8712; s} : Set (Set &#8469;)`</span>
</pre></div>
</div>
<p>Exercise: write down an object of type <code class="docutils literal notranslate"><span class="pre">Set</span> <span class="pre">(Set</span> <span class="pre">(Set</span> <span class="pre">&#8469;))</span></code>.</p>
</section>
<section id="id20">
<h3><span class="section-number">9.3.2. </span>Example<a class="headerlink" href="#id20" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Show that
<span class="math notranslate nohighlight">\(\{n:\mathbb{N}\mid n\text{ is even}\}\notin\{s:\mathcal{P}(\mathbb{N})\mid 3 &#8712;s\}\)</span>.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>We must show 3 is not even.  It suffices to show that 3 is odd.  Indeed, <span class="math notranslate nohighlight">\(3=2\cdot 1+1\)</span>.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="o">{</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">|</span> <span class="n">Nat.Even</span> <span class="n">n</span><span class="o">}</span> <span class="bp">&#8713;</span> <span class="o">{</span><span class="n">s</span> <span class="o">:</span> <span class="n">Set</span> <span class="n">&#8469;</span> <span class="bp">|</span> <span class="mi">3</span> <span class="bp">&#8712;</span> <span class="n">s</span><span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span>
  <span class="n">rw</span> <span class="o">[</span><span class="bp">&#8592;</span> <span class="n">Nat.odd_iff_not_even</span><span class="o">]</span>
  <span class="n">use</span> <span class="mi">1</span>
  <span class="n">numbers</span>
</pre></div>
</div>
</section>
<section id="id21">
<h3><span class="section-number">9.3.3. </span>Example<a class="headerlink" href="#id21" title="Permalink to this headline">&#61633;</a></h3>
<p>Since <span class="math notranslate nohighlight">\(\mathcal{P}(X)\)</span>, the type of sets in <span class="math notranslate nohighlight">\(X\)</span>, is itself a type, we can consider
functions to and from it.</p>
<p>For example, given a set <span class="math notranslate nohighlight">\(s\)</span> of natural numbers, we can build a new set
<span class="math notranslate nohighlight">\(\{n:\mathbb{N}\mid n+1 \in s\}\)</span>.  Lean confirms that this operation (let us call it
<span class="math notranslate nohighlight">\(p\)</span>) is a function from <span class="math notranslate nohighlight">\(\mathcal{P}(\mathbb{N})\)</span> to <span class="math notranslate nohighlight">\(\mathcal{P}(\mathbb{N})\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span> <span class="n">p</span> <span class="o">(</span><span class="n">s</span> <span class="o">:</span> <span class="n">Set</span> <span class="n">&#8469;</span><span class="o">)</span> <span class="o">:</span> <span class="n">Set</span> <span class="n">&#8469;</span> <span class="o">:=</span> <span class="o">{</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">|</span> <span class="n">n</span> <span class="bp">+</span> <span class="mi">1</span> <span class="bp">&#8712;</span> <span class="n">s</span><span class="o">}</span>

<span class="k">#check</span> <span class="bp">@</span><span class="n">p</span> <span class="c1">-- `p : Set &#8469; &#8594; Set &#8469;`</span>
</pre></div>
</div>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Show that the function <span class="math notranslate nohighlight">\(p\)</span> is not injective.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>We must show that there exist sets <span class="math notranslate nohighlight">\(s\)</span> and <span class="math notranslate nohighlight">\(t\)</span>, such that
(i) <span class="math notranslate nohighlight">\(\{n:\mathbb{N}\mid n+1 \in s\} = \{n:\mathbb{N}\mid n+1 \in t\}\)</span>, and
(ii) <span class="math notranslate nohighlight">\(s \ne t\)</span>.</p>
<p>Indeed, let us show that the sets <span class="math notranslate nohighlight">\(\{0\}\)</span> and <span class="math notranslate nohighlight">\(\emptyset\)</span> have this property.  We must
show,
(i) <span class="math notranslate nohighlight">\(\{n:\mathbb{N}\mid n+1 = 0\} = \emptyset\)</span>, and
(ii) <span class="math notranslate nohighlight">\(\{0\} \ne \emptyset\)</span>.</p>
<p>For the first statement, let <span class="math notranslate nohighlight">\(x\)</span> be a natural number.  We must show that <span class="math notranslate nohighlight">\(x+1 \ne 0\)</span>,
which is true since <span class="math notranslate nohighlight">\(x+1 &gt; 0\)</span>.</p>
<p>For the second statement, we must show that there exists a natural number <span class="math notranslate nohighlight">\(k\)</span> such that
<span class="math notranslate nohighlight">\(k\in\{0\}\)</span> and <span class="math notranslate nohighlight">\(k\notin\emptyset\)</span>, or vice versa.  Indeed, <span class="math notranslate nohighlight">\(k=0\)</span> has this
property.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Injective</span> <span class="n">p</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Injective</span><span class="o">,</span> <span class="n">p</span><span class="o">]</span>
  <span class="n">push_neg</span>
  <span class="n">use</span> <span class="o">{</span><span class="mi">0</span><span class="o">},</span> <span class="bp">&#8709;</span>
  <span class="n">dsimp</span>
  <span class="n">constructor</span>
  <span class="bp">&#183;</span> <span class="n">ext</span> <span class="n">x</span>
    <span class="n">dsimp</span>
    <span class="k">suffices</span> <span class="n">x</span> <span class="bp">+</span> <span class="mi">1</span> <span class="bp">&#8800;</span> <span class="mi">0</span> <span class="kd">by</span> <span class="n">exhaust</span>
    <span class="n">apply</span> <span class="n">ne_of_gt</span>
    <span class="n">extra</span>
  <span class="bp">&#183;</span> <span class="n">ext</span>
    <span class="n">push_neg</span>
    <span class="n">use</span> <span class="mi">0</span>
    <span class="n">dsimp</span>
    <span class="n">exhaust</span>
</pre></div>
</div>
</section>
<section id="id22">
<h3><span class="section-number">9.3.4. </span>Example<a class="headerlink" href="#id22" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Consider the function  <span class="math notranslate nohighlight">\(q : \mathcal{P}(\mathbb{Z})\to \mathcal{P}(\mathbb{Z})\)</span> defined by,
<span class="math notranslate nohighlight">\(q(s)=\{n:\mathbb{Z}\mid n+1\in s\}\)</span>. Show that the function <span class="math notranslate nohighlight">\(q\)</span> is injective.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>We must show that for all sets <span class="math notranslate nohighlight">\(s\)</span> and <span class="math notranslate nohighlight">\(t\)</span>,
if <span class="math notranslate nohighlight">\(\{n:\mathbb{Z}\mid n+1 \in s\} = \{n:\mathbb{Z}\mid n+1 \in t\}\)</span>,
then <span class="math notranslate nohighlight">\(s = t\)</span>.</p>
<p>Indeed, let <span class="math notranslate nohighlight">\(s\)</span> and <span class="math notranslate nohighlight">\(t\)</span> be sets and suppose that
<span class="math notranslate nohighlight">\(\{n:\mathbb{Z}\mid n+1 \in s\} = \{n:\mathbb{Z}\mid n+1 \in t\}\)</span>.</p>
<p>Let <span class="math notranslate nohighlight">\(k\)</span> be an integer.
We must show that <span class="math notranslate nohighlight">\(k\in s\)</span> if and only if <span class="math notranslate nohighlight">\(k\in t\)</span>.
Indeed, by the assumption,
<span class="math notranslate nohighlight">\(k -1\in\{n:\mathbb{Z}\mid n+1 \in s\}\)</span> if and only if <span class="math notranslate nohighlight">\(k-1\in \{n:\mathbb{Z}\mid n+1 \in t\}\)</span>.
Simplifying,
<span class="math notranslate nohighlight">\(k -1+1 \in s\)</span> if and only if <span class="math notranslate nohighlight">\(k-1+1\in t\)</span>, and so
<span class="math notranslate nohighlight">\(k  \in s\)</span> if and only if <span class="math notranslate nohighlight">\(k\in t\)</span>.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span> <span class="n">q</span> <span class="o">(</span><span class="n">s</span> <span class="o">:</span> <span class="n">Set</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="o">:</span> <span class="n">Set</span> <span class="n">&#8484;</span> <span class="o">:=</span> <span class="o">{</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="n">n</span> <span class="bp">+</span> <span class="mi">1</span> <span class="bp">&#8712;</span> <span class="n">s</span><span class="o">}</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Injective</span> <span class="n">q</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Injective</span><span class="o">,</span> <span class="n">q</span><span class="o">]</span>
  <span class="n">intro</span> <span class="n">s</span> <span class="n">t</span> <span class="n">hst</span>
  <span class="n">ext</span> <span class="n">k</span>
  <span class="k">have</span> <span class="n">hk</span> <span class="o">:</span> <span class="n">k</span> <span class="bp">-</span> <span class="mi">1</span> <span class="bp">&#8712;</span> <span class="o">{</span><span class="n">n</span> <span class="bp">|</span> <span class="n">n</span> <span class="bp">+</span> <span class="mi">1</span> <span class="bp">&#8712;</span> <span class="n">s</span><span class="o">}</span> <span class="bp">&#8596;</span> <span class="n">k</span> <span class="bp">-</span> <span class="mi">1</span> <span class="bp">&#8712;</span> <span class="o">{</span><span class="n">n</span> <span class="bp">|</span> <span class="n">n</span> <span class="bp">+</span> <span class="mi">1</span> <span class="bp">&#8712;</span> <span class="n">t</span><span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">hst</span><span class="o">]</span>
  <span class="n">dsimp</span> <span class="n">at</span> <span class="n">hk</span>
  <span class="n">conv</span> <span class="n">at</span> <span class="n">hk</span> <span class="bp">=&gt;</span> <span class="n">ring</span>
  <span class="n">apply</span> <span class="n">hk</span>
</pre></div>
</div>
</section>
<section id="id23">
<h3><span class="section-number">9.3.5. </span>Example<a class="headerlink" href="#id23" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Let <span class="math notranslate nohighlight">\(X\)</span> be a type.  Prove that there does not exist a surjective function from  <span class="math notranslate nohighlight">\(X\)</span> to
<span class="math notranslate nohighlight">\(\mathcal{P}(X)\)</span>.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>Suppose for the sake of contradiction that some function <span class="math notranslate nohighlight">\(f:X\to\mathcal{P}(X)\)</span> were
surjective.  We introduce the
following set in <span class="math notranslate nohighlight">\(X\)</span>:</p>
<div class="math notranslate nohighlight">
\[s :=\{x:X\mid x\notin f(x)\}.\]</div>
<p>Since <span class="math notranslate nohighlight">\(f\)</span> is surjective, there exists some <span class="math notranslate nohighlight">\(x\)</span> of type <span class="math notranslate nohighlight">\(X\)</span> such that
<span class="math notranslate nohighlight">\(f(x)=s\)</span>. We consider cases according to whether <span class="math notranslate nohighlight">\(x\in s\)</span>.</p>
<p><strong>Case 1</strong> (<span class="math notranslate nohighlight">\(x\in s\)</span>):  Then by the definition of <span class="math notranslate nohighlight">\(s\)</span>, it is true that
<span class="math notranslate nohighlight">\(x\notin f(x)\)</span>, so since <span class="math notranslate nohighlight">\(f(x)=s\)</span>, we have <span class="math notranslate nohighlight">\(x\notin s\)</span>, contradiction.</p>
<p><strong>Case 2</strong> (<span class="math notranslate nohighlight">\(x\notin s\)</span>):  Then by the definition of <span class="math notranslate nohighlight">\(s\)</span>, it is false that
<span class="math notranslate nohighlight">\(x\notin f(x)\)</span>, so since <span class="math notranslate nohighlight">\(f(x)=s\)</span>, we have that it is false that <span class="math notranslate nohighlight">\(x\notin s\)</span>,
contradiction.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="bp">&#8707;</span> <span class="n">f</span> <span class="o">:</span> <span class="n">X</span> <span class="bp">&#8594;</span> <span class="n">Set</span> <span class="n">X</span><span class="o">,</span> <span class="n">Surjective</span> <span class="n">f</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">intro</span> <span class="n">h</span>
  <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">f</span><span class="o">,</span> <span class="n">hf</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">h</span>
  <span class="k">let</span> <span class="n">s</span> <span class="o">:</span> <span class="n">Set</span> <span class="n">X</span> <span class="o">:=</span> <span class="o">{</span><span class="n">x</span> <span class="bp">|</span> <span class="n">x</span> <span class="bp">&#8713;</span> <span class="n">f</span> <span class="n">x</span><span class="o">}</span>
  <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">x</span><span class="o">,</span> <span class="n">hx</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">hf</span> <span class="n">s</span>
  <span class="n">by_cases</span> <span class="n">hxs</span> <span class="o">:</span> <span class="n">x</span> <span class="bp">&#8712;</span> <span class="n">s</span>
  <span class="bp">&#183;</span> <span class="k">have</span> <span class="n">hfx</span> <span class="o">:</span> <span class="n">x</span> <span class="bp">&#8713;</span> <span class="n">f</span> <span class="n">x</span> <span class="o">:=</span> <span class="n">hxs</span>
    <span class="n">rw</span> <span class="o">[</span><span class="n">hx</span><span class="o">]</span> <span class="n">at</span> <span class="n">hfx</span>
    <span class="n">contradiction</span>
  <span class="bp">&#183;</span> <span class="k">have</span> <span class="n">hfx</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">x</span> <span class="bp">&#8713;</span> <span class="n">f</span> <span class="n">x</span> <span class="o">:=</span> <span class="n">hxs</span>
    <span class="n">rw</span> <span class="o">[</span><span class="n">hx</span><span class="o">]</span> <span class="n">at</span> <span class="n">hfx</span>
    <span class="n">contradiction</span>
</pre></div>
</div>
<p>The idea behind this twisty proof is sometimes called the
<a class="reference external" href="https://en.wikipedia.org/wiki/Barber_paradox">barber paradox</a>.  Here is the version featuring
barbers.  There is a town with a barber, and in this town, the barber shaves all men who don&#8217;t shave
themselves.  Paradox: does the barber shave himself?</p>
</section>
<section id="id24">
<h3><span class="section-number">9.3.6. </span>Exercises<a class="headerlink" href="#id24" title="Permalink to this headline">&#61633;</a></h3>
<ol class="arabic">
<li><p>Consider the function <span class="math notranslate nohighlight">\(r : \mathcal{P}(\mathbb{N})\to \mathcal{P}(\mathbb{N})\)</span> defined by,
<span class="math notranslate nohighlight">\(r(s)=s\cup \{3\}\)</span>.  Show that <span class="math notranslate nohighlight">\(r\)</span> is not injective.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span> <span class="n">r</span> <span class="o">(</span><span class="n">s</span> <span class="o">:</span> <span class="n">Set</span> <span class="n">&#8469;</span><span class="o">)</span> <span class="o">:</span> <span class="n">Set</span> <span class="n">&#8469;</span> <span class="o">:=</span> <span class="n">s</span> <span class="bp">&#8746;</span> <span class="o">{</span><span class="mi">3</span><span class="o">}</span>

<span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Injective</span> <span class="n">r</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Consider the sequence <span class="math notranslate nohighlight">\(U_n\)</span> of sets of integers defined recursively by,</p>
<div class="math notranslate nohighlight">
\[\begin{split}U_0&amp;=\mathbb{Z} \\
\text{for }n:\mathbb{N},\quad U_{n+1} &amp;=\{x:\mathbb{Z}\mid \exists \ y\in U_n, x = 2y \}\end{split}\]</div>
<p>Show that for all natural numbers <span class="math notranslate nohighlight">\(n\)</span>, <span class="math notranslate nohighlight">\(U_n=\{x:\mathbb{Z}\mid 2^n\mid x\}\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span> <span class="n">U</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">&#8594;</span> <span class="n">Set</span> <span class="n">&#8484;</span>
  <span class="bp">|</span> <span class="mi">0</span> <span class="bp">=&gt;</span> <span class="n">univ</span>
  <span class="bp">|</span> <span class="n">n</span> <span class="bp">+</span> <span class="mi">1</span> <span class="bp">=&gt;</span> <span class="o">{</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="bp">&#8707;</span> <span class="n">y</span> <span class="bp">&#8712;</span> <span class="n">U</span> <span class="n">n</span><span class="o">,</span> <span class="n">x</span> <span class="bp">=</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">y</span><span class="o">}</span>

<span class="kd">example</span> <span class="o">(</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8469;</span><span class="o">)</span> <span class="o">:</span> <span class="n">U</span> <span class="n">n</span> <span class="bp">=</span> <span class="o">{</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="o">(</span><span class="mi">2</span><span class="o">:</span><span class="n">&#8484;</span><span class="o">)</span> <span class="bp">^</span> <span class="n">n</span> <span class="bp">&#8739;</span> <span class="n">x</span><span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">simple_induction</span> <span class="n">n</span> <span class="k">with</span> <span class="n">k</span> <span class="n">hk</span>
  <span class="bp">&#183;</span> <span class="n">rw</span> <span class="o">[</span><span class="n">U</span><span class="o">]</span>
    <span class="gr">sorry</span>
  <span class="bp">&#183;</span> <span class="n">rw</span> <span class="o">[</span><span class="n">U</span><span class="o">]</span>
    <span class="n">ext</span> <span class="n">x</span>
    <span class="n">dsimp</span>
    <span class="gr">sorry</span>
</pre></div>
</div>
</li>
</ol>
<p class="rubric">Footnotes</p>
<dl class="footnote brackets">
<dt class="label" id="id25"><span class="brackets"><a class="fn-backref" href="#id19">1</a></span></dt>
<dd><p>In set theory, which we <em>don&#8217;t</em> use as the logical foundation of this book,
<span class="math notranslate nohighlight">\(\mathcal{P}(X)\)</span> is referred to as
the <em>power set</em> of <span class="math notranslate nohighlight">\(X\)</span>.  Maybe in type theory we should refer to it as the &#8220;power type&#8221; of
<span class="math notranslate nohighlight">\(X\)</span> &#8230;?</p>
</dd>
</dl>
</section>
</section>
</section>


           </div>
          </div>
          <footer><div class="rst-footer-buttons" role="navigation" aria-label="Footer">
        <a href="08_Functions.html" class="btn btn-neutral float-left" title="8. Functions" accesskey="p" rel="prev"><span class="fa fa-arrow-circle-left" aria-hidden="true"></span> Previous</a>
        <a href="10_Relations.html" class="btn btn-neutral float-right" title="10. Relations" accesskey="n" rel="next">Next <span class="fa fa-arrow-circle-right" aria-hidden="true"></span></a>
    </div>

  <hr/>

  <div role="contentinfo">
    <p>&#169; Copyright 2022-2024, Heather Macbeth.  All rights reserved.</p>
  </div>

  Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
    <a href="https://github.com/readthedocs/sphinx_rtd_theme">theme</a>
    provided by <a href="https://readthedocs.org">Read the Docs</a>.
   

</footer>
        </div>
      </div>
    </section>
  </div>
  <script>
      jQuery(function () {
          SphinxRtdTheme.Navigation.enable(true);
      });
  </script> 

</body>
</html>